Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Do not run the
diff
GA workflow on closed PRs.
The `diff.yml` GitHub Actions workflow runs whenever a new comment is added to a PR, to check whether the comment contains a `gogoeditdiff` tag that asks for the production of a diff. Unfortunately, one of the actions this workflow is dependent on does not handle correctly the case where the PR has been closed but is still commented on, and throws an error when that happens. So we add an additional condition before running the workflow: the PR has to be open. This will prevent people from requesting a diff in a closed PR, but: (1) this should not be something that people would need often (if the PR has been closed, why would a diff be required); (2) if a diff _is_ required on a closed PR, it is always possible to re-open the PR (arguably this is what should be done anyway: if someone is interested in the PR enough for wanting a diff and checking what are its consequences on the ontology, that sounds like a sign that the PR is not worthless and should be kept open); (3) in any case, in the current situation requesting a diff on a closed PR already does not work anyway, since the action we are dependent does not know how to work on a closed PR. The main interest of this change is to avoid receiving needless emails letting us know that a workflow has failed, just because people are commenting on a closed PR.
- Loading branch information