Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
GitHub Actions: trigger CI only on 'master' branch, tags, and pull re…
…quests We do not want CI to be performed twice for a pull request from the same repository: once for a push to a branch and once for a pull request.
- Loading branch information