diff options
| author | Boris Kolpackov <boris@codesynthesis.com> | 2024-11-04 11:53:16 +0200 |
|---|---|---|
| committer | Boris Kolpackov <boris@codesynthesis.com> | 2024-11-04 11:53:16 +0200 |
| commit | 486fe4de562d88d15ee44febf2ebd12d6b0db492 (patch) | |
| tree | 36a2dc9bad7f52cf65162cc8b73437d52d8d50a4 /doc | |
| parent | 547ec84687f763ae645d3df6f2993d619add2fad (diff) | |
Minor tweaks
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/manual.cli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/doc/manual.cli b/doc/manual.cli index ce9a698..f9af78d 100644 --- a/doc/manual.cli +++ b/doc/manual.cli @@ -783,13 +783,13 @@ changes uncompilable or otherwise buggy once merged. The second representative example is a single remote PR: someone creates a PR with a feature or bugfix from their fork of our repository. There is no corresponding branch push for this PR's head commit in our repository so it -sounds like there is only one place (the PR) where the CI result of the head -commit (@@ Shouldn't this be `merge commit`?) will be reported in our repository and so the head sharing should not -be an issue, right? While it's true that \i{spatial} sharing, that is between -BP and/or several PRs, is not an issue in this case, \i{temporal} sharing -still is. Specifically, if the base branch moves before we examine the PR, we -again may end up merging it based on the CI results that are not -representative of the merge commit. +sounds like there is only one place (the PR) where the CI result, if +associated with this head commit, will be reported in our repository and so +the head sharing should not be an issue, right? While it's true that +\i{spatial} sharing, that is between BP and/or several PRs, is not an issue in +this case, \i{temporal} sharing still is. Specifically, if the base branch +moves before we examine the PR, we again may end up merging it based on the CI +results that are not representative of the merge commit. Hopefully you see the underlying theme by now: the only way to ensure correctness in the GitHub CI model is to make sure the PR's head and merge |