The companion tool `tools/reset-to-pull-request` has a handy feature
to maintain a local ref tracking the PR: e.g., pr/1234 for PR 1234.
If this were a normal remote-tracking branch maintained by `git fetch`,
it'd get updated on `git push`. Do the same thing here.
This helps keep a view like `gitk --all @` a bit tidier, by causing
merged PRs to stop pointing at side branches of the main history.
The appropriate name for the remote pointing at the repo we maintain
may be `upstream` for most of our repos... but not when we're
downstream of someone else, e.g. for react-native. So, make it easy
to configure per-repo.
This option (aka `--raw-output`) prints a string as itself, rather
than JSON-encoded; which makes it fit a bit better in a shell script,
saving us a layer of quoting.
This replaces ad4617c95 with a different fix for the same issue:
instead of stripping the `.git` off separately, we can just correct
the regex, using `+?` to fix our stepping in a classic regex pitfall.
I've often done this by hand -- basically typed out the last line,
with the variables found from looking at the PR page in a browser.
Seems nicer for both us maintainers and the contributor, in particular
because the PR gets marked as merged, instead of closed. But it's a
bit of a pain, and I do it maybe half the time or less; plus it's kind
of a subtle GitHub feature, and as a result I think other maintainers
of Zulip repos do this approximately never.
I've always figured this couldn't be hard to automate; today I decided
to take the 45 minutes to look up how, write out the script, QA it,
write up a nice usage message and some comments, and commit it. :)
Greg Price
Tim Abbott