diff options
| author | Boris Kolpackov <boris@codesynthesis.com> | 2024-11-05 10:05:01 +0200 |
|---|---|---|
| committer | Boris Kolpackov <boris@codesynthesis.com> | 2024-11-05 10:05:01 +0200 |
| commit | cd9a4cc2fac01c1e7acf726edd5741d74605a9b3 (patch) | |
| tree | 305abada0f1c98a13a9066fbf595e2d629a8ce74 /doc | |
| parent | 451fb4ab1466a86c60b1900374b4d822d020471b (diff) | |
Minor addition to documentation
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/manual.cli | 11 |
1 files changed, 11 insertions, 0 deletions
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. + " |