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.

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

Change CI configuration #25

Merged
merged 1 commit into from
Apr 6, 2023
Merged

Change CI configuration #25

merged 1 commit into from
Apr 6, 2023

Conversation

bquorning
Copy link

on: [push, pull_request] caused us to run each job twice every time someone push a commit to an open pull request.

With the new configuration, we run CI once when opening a PR, and once when pushing a commit that belongs to a pull request. And once when merging to master (the push event). Importantly, this configuration still works for contributions from forked repositories, since the pull_request events are triggered on our fork.

@bquorning bquorning marked this pull request as ready for review April 5, 2023 14:42
1. Fix indentation (according to yamllint)
2. Don't run CI on all push & pull request events. Pushing a commit to an open
   pull request would run each job twice.

   With the new configuration, we run CI once when opening a PR, and once when
   pushing a commit that belongs to a pull request. And once when merging to
   master (the `push` event). Importantly, this configuration still works for
   contributions from forked repositories, since the `pull_request` events are
   triggered on _our_ fork.
@bquorning
Copy link
Author

Fixes #10.

@bquorning bquorning merged commit b2949ff into master Apr 6, 2023
@bquorning bquorning deleted the change-ci-configuration branch April 6, 2023 05:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants