On Tue, 6 Apr 2021, 08:15 antonio, <[email protected]> wrote: > c) Otherwise we committers can squash using the command line with the > detailed instructions that Matthias suggested on 2019-12-12 ([1]). > > Am I understading this correctly? >
Ideally not from step 14. Instead, git push -f to the pull request, then merge as normal. Obviously good to check with PR author where possible as you're pushing to their repo. Then they can check, and we don't lose the link with the PR. Best wishes, Neil >
