From cd9a4cc2fac01c1e7acf726edd5741d74605a9b3 Mon Sep 17 00:00:00 2001 From: Boris Kolpackov Date: Tue, 5 Nov 2024 10:05:01 +0200 Subject: Minor addition to documentation --- doc/manual.cli | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'doc') diff --git a/doc/manual.cli b/doc/manual.cli index f9af78d..a550e5a 100644 --- a/doc/manual.cli +++ b/doc/manual.cli @@ -817,4 +817,15 @@ create a PR from a local feature branch, you may immediately see the successful CI result because it is the same as for the branch push to the feature branch. +Finally note that the GitHub CI model is quite wasteful of CI resources in +general and the head sharing makes this problem even worse. Specifically, +GitHub CI builds every commit indiscriminately, regardless of what was +changed. So a minor tweak to \c{README.md} will trigger a full rebuild even +though nothing that needs building has changed. The head sharing issue makes +the situation worse because the CI integration cannot easily cancel an +in-progress build when a new commit is added to a PR because the result could +be shared with a branch push or another PR. Nevertheless, this integration +will attempt to cancel a stale build of a remote PR provided it's not +(currently) shared. + " -- cgit v1.1