diff options
author | Boris Kolpackov <boris@codesynthesis.com> | 2024-11-26 11:11:11 +0200 |
---|---|---|
committer | Boris Kolpackov <boris@codesynthesis.com> | 2024-12-10 16:44:55 +0200 |
commit | 07003c825d632662ea9905c3d14af44710a640e0 (patch) | |
tree | 1ecf74d0605fa9da37052de3031ab07b2d1d28a9 /mod/mod-ci-github-gh.hxx | |
parent | 475771f84d3fb6197fea772d67e5a59c46b512e5 (diff) |
Remote PRs: cancel previous PR head commit CI
Diffstat (limited to 'mod/mod-ci-github-gh.hxx')
-rw-r--r-- | mod/mod-ci-github-gh.hxx | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/mod/mod-ci-github-gh.hxx b/mod/mod-ci-github-gh.hxx index b29904b..6ede697 100644 --- a/mod/mod-ci-github-gh.hxx +++ b/mod/mod-ci-github-gh.hxx @@ -183,6 +183,12 @@ namespace brep string action; gh_pull_request pull_request; + + // The SHA of the previous commit on the head branch before the current + // one. Only present if action is "synchronize". + // + optional<string> before; + gh_repository repository; gh_installation installation; |