Do not run the diff
GA workflow on closed PRs.
#3437
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The
diff.yml
GitHub Actions workflow runs whenever a new comment is added to a PR, to check whether the comment contains agogoeditdiff
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.