To force-push or not to force-push

[Rainer Müller]

On 2017-04-15 21:30, Mojca Miklavec wrote:
> 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

For pull requests, you are not pushing to the MacPorts repository, but
to the repository of the user who opened the pull request...

It seems like it would be easier to correct these kind of things if we
allowed squashing commits in the GitHub UI when accepting a pull
request, instead of only allowing rebase.

Rainer