Duplicate CI pipeline jobs

[sebastianbergmann]

When I push to a branch in this repository which is used in a pull request in this repository then the CI pipeline is run twice: once triggered by the push event and once triggered by the pull_request event:

It would be nice if the CI pipeline would only be run once in this case. If this is possible at all then we should only build for pull_request (so that the information in the pull request is updated) and not for push.

[talkinnl]

  push:
    branches:
      - 'main'
      - 'releases/**'

Example syntax to restrict the push workflow.

I can make a PR for this. :)

[talkinnl]

I thought of this:

on:
  pull_request:
    branches:
      - main
      - "[0-9]*"
  push:
  schedule:
    - cron: "15 0 * * *"

i.e. add a branch restriction for main or any of your branches starting with version number.

But this won't work, as I see internal branches with arbitrary patterns.

I see a hack at https://stackoverflow.com/a/65946732 , but I don't like that.

So I guess it's actually not that easy? Not de-duplicating on the commit hash seems just wasteful of Github.