Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Renintroduce
pull_request
in GitHub workflow with if case
The disadvantage of removing the `pull_request` as trigger event for an GitHub workflow is that it does not trigger for pushes from a foreign repo. To run the workflow also in this case without running the workflow twice for PRs based on the original repo we introduce an if case that runs the `pull_request` event only when it from a foreign repo.
- Loading branch information