Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Tweak CI: remove on push for PRs and add names to CI steps #37

Merged
merged 2 commits into from
Jul 4, 2024
Merged

Tweak CI: remove on push for PRs and add names to CI steps #37

merged 2 commits into from
Jul 4, 2024
+11 −5

Commits on Jul 4, 2024

  1. Add names to CI steps

    Mattijs Kneppers committed Jul 4, 2024
    Configuration menu
    Copy the full SHA
    a685a3c View commit details
    Browse the repository at this point in the history

  2. ci: remove on push 

    We included `push` to make sure PRs get tested when new commits were added or the commit history was changed. However, it appears that for an active PR, every push already causes a `synchronize` activity type for the `pull_request_target` event.

So the `push` event is no longer needed for every PR. Instead, this sets it to trigger only for the case when something was pushed directly to `main`.

See:
https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#pull_request_target
    Mattijs Kneppers committed Jul 4, 2024
    Configuration menu
    Copy the full SHA
    239cf9b View commit details
    Browse the repository at this point in the history