And link to it from the GitHub guide. Since it fits in the flow of the
former document better, but is of interest to those using the GitHub
specific guide.
This includes some content I wrote for an automated PR comment but I
think is useful to have in a single place to link to instead.
I have removed some details:
* About the waterfall view because it doesn't seem that useful to new
contributors and is likely to just seem like constant chaos given how
many builds are going on.
* The orange bubbles in the console view. I also remember this being the
case but whether it was changed, or the web UI is just not loading
properly, I now see red builds that were red before that commit. So
again, it seems like detail that's not needed for a new contributor.
We used to support a /branch comment to specify a branch with commits to
backport to the release branch. However, now that we can use pull
requests this is not needed.
This also simplifies the process, because now the cherry-pick job can
create the pull request directly instead of having it split across two
separate jobs.
GitHub will use the first line of the commit as the title for a
single-commit PR, but truncates it at 72 characters
<https://github.com/orgs/community/discussions/12450>. This truncation
makes the PRs less readable if not manually undone, and even worse, the
truncated form may survive through to commit if "Squash and rebase" is
used in the GitHub web UI. From preparing LLVM Weekly, I've seen this a
number of times and it really does make it more annoying to flick
through commits.
I'm not sure if this is the best place for the guidance, or whether you
get the same behaviour when creating a PR with `gh`, but I'm quite keen
we give a warning of some sort about this behaviour.
The documentation for how to use "gh pr merge" was broken.
In one place it said '--delete-branch' (which seem to be correct for
that option). But in second place it said '--delete branch' and in a
third place it just said '--delete'.
Make sure '--delete-branch' is used in all three places.
I recently went to merge a PR that had a merge conflict:
$ gh pr merge --squash --delete-branch
X Pull request #66003 is not mergeable: the merge commit cannot be
cleanly created.
To have the pull request merged after all the requirements have been
met, add the `--auto` flag.
Run the following to resolve the merge conflicts locally:
gh pr checkout 66003 && git fetch origin main && git merge origin/main
This is how I resolved it; we should recommend this explicitly for
fellow contributors.
Some people may not have access to `gh` or may prefer to use `git` and
the GitHub web interface to make a PR. This patch adds an example of
making a PR using this approach.
This adds first version of a GitHub workflow in the documentation and marks some
sections as deprecated. We should clean up these sections ASAP. I was
just keen to get something on the documentation site as soon as
possible.
