Skip to content

Skip unnecessary CI runs for PRs from same user#87

Merged
Sergio0694 merged 1 commit into
mainfrom
dev/skip-repeated-pr-ci-runs
Oct 28, 2023
Merged

Skip unnecessary CI runs for PRs from same user#87
Sergio0694 merged 1 commit into
mainfrom
dev/skip-repeated-pr-ci-runs

Conversation

@Sergio0694

Copy link
Copy Markdown
Owner

Description

This PR updates the CI script so that it only runs for pushes, or for published PRs from other forks of this repo.

@Sergio0694 Sergio0694 added the infrastructure Build/packaging related changes label Oct 28, 2023
@Sergio0694 Sergio0694 force-pushed the dev/skip-repeated-pr-ci-runs branch from 39a7656 to 353548c Compare October 28, 2023 10:45
@Sergio0694 Sergio0694 merged commit 7e367d3 into main Oct 28, 2023
@Sergio0694 Sergio0694 deleted the dev/skip-repeated-pr-ci-runs branch October 28, 2023 10:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

infrastructure Build/packaging related changes

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant