Skip to content

Improve CI#52

Merged
devmotion merged 2 commits intomasterfrom
dw/ci
Feb 10, 2022
Merged

Improve CI#52
devmotion merged 2 commits intomasterfrom
dw/ci

Conversation

@devmotion
Copy link
Member

This PR

@devmotion devmotion requested a review from sethaxen February 9, 2022 21:36
- push
- pull_request
push:
branches: [master]
Copy link
Member

@sethaxen sethaxen Feb 9, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Perhaps we should also run on tagged versions?

Suggested change
branches: [master]
branches: [master]
tags: [v*]

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't mind. But I don't think it is necessary - it is run for every commit pushed to the master branch anyway. I think the tags trigger is mainly useful for building release-specific documentation.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We'll want that eventually anyways, once we have documentation. I'll leave it up to you whether to add it.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For documentation we might want to add a separate action anyway, IMO that's cleaner (and e.g. allows more fine-tuned triggers) 🤷

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't add the trigger in this PR, we can add it later if it seems useful.

Comment on lines +8 to +12
concurrency:
# Skip intermediate builds: always.
# Cancel intermediate builds: only if it is a pull request build.
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: ${{ startsWith(github.ref, 'refs/pull/') }}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, I hadn't seen this done before. I assume you've seen it in action and it works as documented.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@devmotion devmotion merged commit 12a0e27 into master Feb 10, 2022
@devmotion devmotion deleted the dw/ci branch February 10, 2022 00:08
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.

2 participants