diff options
| author | Boris Kolpackov <boris@codesynthesis.com> | 2024-11-27 11:41:23 +0200 |
|---|---|---|
| committer | Boris Kolpackov <boris@codesynthesis.com> | 2024-12-10 16:44:55 +0200 |
| commit | 0dd483c8d91fc895b1669389f453fb98f1c64bd3 (patch) | |
| tree | 9315e370809ba80783bc9b5b56983960011691f0 /mod | |
| parent | 583d74bc0dc8003eb69b24eacdb8777104fa6b2f (diff) | |
Handle close/reopen PR actions
Diffstat (limited to 'mod')
| -rw-r--r-- | mod/mod-ci-github.cxx | 21 |
1 files changed, 16 insertions, 5 deletions
diff --git a/mod/mod-ci-github.cxx b/mod/mod-ci-github.cxx index d9a84f8..46cd0cc 100644 --- a/mod/mod-ci-github.cxx +++ b/mod/mod-ci-github.cxx @@ -424,21 +424,30 @@ namespace brep // relying instead on the branch protection rule. So it makes sense // to do the same here. // - return true. + return true; } else if (pr.action == "closed") { // PR has been closed (as merged or not; see merged member). Also - // apparently received if base branch is deleted. (And presumably same - // for head branch.) See also the reopened event below. + // apparently received if base branch is deleted (and the same + // for head branch). See also the reopened event below. // - - // Cancel CI? + // While it may seem natural to cancel the CI for the closed PR, it + // might actually be useful to have a completed CI record. GitHub + // doesn't prevent us from publishing CI results for the closed PR + // (even if both base and head branches were deleted). And if such a + // PR is reopened, the CI results remain. + // + return true; } else if (pr.action == "reopened") { // Previously closed PR has been reopened. // + // Since we don't cancel the CI for a closed PR, there is nothing + // to do if it is reopened. + // + return true; } else if (pr.action == "assigned" || pr.action == "auto_merge_disabled" || @@ -458,6 +467,8 @@ namespace brep pr.action == "unlocked") { // These have no relation to CI. + // + return true; } else { |