Am 29.04.2015 um 06:50 schrieb Cédric Champeau:
There's no such thing as write access to the mirror, even for closing PRs.
You have to submit a dummy commit with something recognized by GitHub as a
message to close a PR. For example "Closes #3". Since such dummy commits
pollute the history, my suggestion would be that before merging a PR, we do
an interactive rebase and reword the last commit to include this.
Hope this helps.
Hi Cédric,
thanks for the information.
Modifying a commit by another person seems a bit "unethical" to me, but
if there is no better option it will have to do.
-Pascal
