From 0dd483c8d91fc895b1669389f453fb98f1c64bd3 Mon Sep 17 00:00:00 2001 From: Boris Kolpackov Date: Wed, 27 Nov 2024 11:41:23 +0200 Subject: Handle close/reopen PR actions --- mod/mod-ci-github.cxx | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) (limited to 'mod') 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 { -- cgit v1.1