To force-push or not to force-push

[Mojca Miklavec]

Hi,

A confused maintainer just pointed out "a problem" with our guidelines:
     https://trac.macports.org/wiki/CommitMessages#corrections

~~~
You cannot correct commits that you have already pushed. Comment on
the commit's GitHub page instead. (Modifying your local history causes
it to diverge from the public history. Publishing this alternate
history would require force-pushing, which we disallow because it's
bad practice.)
~~~

However this does NOT hold for pull requests and we really need to clarify this.

https://github.com/macports/macports-ports/pull/421#issuecomment-294312952

Mojca