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

Remove unnecessary if in the user guide workflow #8019

Merged
merged 1 commit into from
Feb 28, 2022

Conversation

jneira
Copy link
Member

@jneira jneira commented Feb 28, 2022

As github already is not triggering workflows for commits with skip ci as demonstrated here: #6200

@jneira jneira requested a review from andreasabel February 28, 2022 09:08
@andreasabel
Copy link
Member

The official reference seems to be this: https://github.blog/changelog/2021-02-08-github-actions-skip-pull-request-and-push-workflows-with-skip-ci/

GitHub Actions now supports skipping push and pull_request workflows by looking for some common keywords in your commit message.
If any commit message in your push or the HEAD commit of your PR contains the strings [skip ci], [ci skip], [no ci], [skip actions], or [actions skip] workflows triggered on the push or pull_request events will be skipped.

@andreasabel andreasabel added merge me Tell Mergify Bot to merge and removed attention: needs-review labels Feb 28, 2022
As github already is not triggering workflows for commits with skip ci
@jneira jneira force-pushed the jneira/remove-unnecessary-if-workflow branch from a7a1f3d to 477696e Compare February 28, 2022 14:40
@mergify mergify bot merged commit 632571c into master Feb 28, 2022
@jneira jneira deleted the jneira/remove-unnecessary-if-workflow branch February 28, 2022 17:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
merge me Tell Mergify Bot to merge
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants