GitHub migration complete

[Marko Käning]

Hi Larry,

On 31 Oct 2016, at 05:38 , Lawrence Velázquez <larryv at macports.org> wrote:
> Old habits die hard, but from now on do NOT refer to Trac tickets as
> "#12345" in your commit messages; GitHub's website interprets those as
> pull request numbers. Copy and paste the full Trac URL instead.

a post-commit-hook checking whether the GitHub pull request ID #123
actually exists for the main repository seems like a valuable feature,
especially in the transition phase. Shall I file a ticket on trac for it?

Greets,
Marko