> On Dec 6, 2016, at 10:33 AM, Rainer Müller <rai...@macports.org> wrote: > > (e) add "Closes: #XYZ" to the commit message
When commits close PRs implicitly (by merging the PR branch) instead of explicitly (by using "closes #XYZ" in the message), the PR is remembered internally by GitHub and displayed on the website but is not recorded in our Git repository. If we ever migrate off GitHub, we would presumably lose this information. Should we consider this a problem? vq
