Avoid duplicate Action-runs after PR merges #3546

Actions are a great feature, but one thing that has always annoyed me are duplicate Action-runs after PR merges. A duplicate Action-run happens if an Action has successfully passed on a "feature branch", but the Action is then repeated on the "master branch" right after merging the "feature branch". Right after the merge, this repetition is unnecessary because the contents of the "feature branch" and the "master branch" are exactly the same (with some exceptions, see below for technical details). Duplicate Action-runs do not only add noise to the Action-history, but also increase cost for enterprise users.

To understand the following explanation in detail, you need some expert knowledge about Git-internals (but this is something that I expect from GitHub):

• I differentiate PR merges into trivial merges and non-trivial merges.
• I define a trivial merge as a merge where the "master branch" ends up with the same tree hash as the merged "feature branch" (after the merge is done).
• In contrast, a non-trivial merge is a merge where the "master branch" ends up with a different tree hash than the merged "feature branch". For example, this can happen if the "master branch" changed after the "feature branch" was submitted.
• For non-trivial merges, it is necessary to repeat GitHub actions after the merge (GitHub does this correctly).
• However, for trivial merges, repeating GitHub actions on the "master branch" is wasted time. Instead, a green checkbox should be instantly taken over from the merged feature branch.
• A trivial merge is not necessarily a fast-forward merge. It is common to do squash-merges or rebase-merges that are still trivial merges. The only thing that matters is the resulting tree hash after the merge; not the exact details on how the merge is done.

Note that I refer to actions with a push trigger in their yml-file, like so:

on:
  push:
    branches:
      - '**'