Commit Graph

20 Commits

Author SHA1 Message Date
Anders Kaseorg 646c04eff2 Rename default branch to ‘main’.
Signed-off-by: Anders Kaseorg <anders@zulip.com>
2021-09-06 12:56:35 -07:00
Anders Kaseorg 47897c76a2 scripts: Use curl -f (--fail).
This makes curl exit with nonzero status on HTTP 4xx/5xx errors.

Signed-off-by: Anders Kaseorg <anders@zulip.com>
2021-07-13 16:47:49 -07:00
Anders Kaseorg 4bcf7131c1 push-to-pull-request: Wait for GitHub background update before merge.
Signed-off-by: Anders Kaseorg <anders@zulip.com>
2021-02-03 14:55:08 -08:00
Anders Kaseorg 50121cce5e push-to-pull-request: Add --merge option.
Signed-off-by: Anders Kaseorg <anders@zulip.com>
2021-01-22 18:00:25 -08:00
Anders Kaseorg 26a7b7196c push-to-pull-request: Use getopt.
Signed-off-by: Anders Kaseorg <anders@zulip.com>
2021-01-22 18:00:25 -08:00
Anders Kaseorg dfaea9df65 shfmt: Reformat shell scripts with shfmt.
https://github.com/mvdan/sh

Signed-off-by: Anders Kaseorg <anders@zulip.com>
2020-10-15 15:16:00 -07:00
Greg Price 1e2b558b01 reset-to-pull-request: Add a usage message.
Every CLI program should have a usage message.

Also add a mention in the `push-to-pull-request` usage message of
its participation in the `refs/remotes/pr/` pseudo-remote feature.
2020-02-11 14:45:17 -08:00
Greg Price e3d843baf9 push-to-pull-request: Give a more detailed error on URL parse failure.
This simplifies debugging when this error fires, e.g. for finding
an issue like the one we just used `git remote get-url` to fix.
2020-02-11 14:45:17 -08:00
Greg Price e7a82e732e push-to-pull-request: Use `git remote get-url`.
This gives us the right behavior when using the `url.*.insteadOf`
mechanism for aliases in Git remote URLs.  For example, if
one's ~/.gitconfig has:

  [url "git@github.com:"]
      insteadOf = gh:

then `git remote add upstream gh:zulip/zulip` will work great, as
the nice, short, mnemonic `gh:` prefix gets expanded to the more
finicky `git@github.com:`.  I use just such a prefix routinely.

But the feature does require that scripts go through the right
abstractions.  In particular `git remote get-url`, since Git 2.7
(from 2016), exists for exactly this reason.  A plain `git config`
command bypasses the expansion, getting the verbatim `gh:...`
version, which doesn't work.

So, switch to that.

As a bonus, we get to behave correctly if for some reason the user
has configured a push URL distinct from the fetch URL for this
remote, just by adding `--push`.  With `git config`, we'd have had
to manually implement the fallback from `remote.upstream.pushUrl` to
`remote.upstream.url` in order to properly handle that case.
2020-02-11 14:45:17 -08:00
Anders Kaseorg 392175d6e8 Use #!/usr/bin/env for bash shebangs.
/bin/sh and /usr/bin/env are the only two binaries that NixOS provides
at a fixed path (outside a buildFHSUserEnv sandbox).

This discussion was split from #11004.

Signed-off-by: Anders Kaseorg <andersk@mit.edu>
2018-12-17 17:21:08 -08:00
Greg Price 3b646c5d28 push-to-pull-request: Update local tracking ref, if any.
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.
2018-09-25 13:15:02 -07:00
Greg Price 79dfe6e0ae push-to-pull-request: Fix shell usage in an error path.
Errors go to stderr, not stdout.

While we're here, match the message itself to the others in
this script.
2018-07-23 23:19:27 -07:00
Greg Price 26d0904436 push-to-pull-request: Give a nice error if `jq` missing. 2018-07-23 23:19:27 -07:00
Greg Price 0462e85d02 tools: Make remote configurable in {reset,push}-to-pull-request.
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.
2018-06-21 17:28:21 -07:00
Greg Price f686d55fa0 push-to-pull-request: Broaden one error message.
I discovered this case just now while testing other changes.
2018-06-01 16:52:18 -07:00
Greg Price 954c71e90c push-to-pull-request: Use `jq -r` to simplify a test slightly.
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.
2018-06-01 16:52:18 -07:00
Greg Price 8e81ca0fb2 push-to-pull-request: Fix regex usage in parsing remote.
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.
2018-06-01 16:52:18 -07:00
Tim Abbott 60eae53327 push-to-pull-request: Provide better output for invalid PR.
Previously, we were very confusingly showing the error message for
permissions when the issue was a not-found error.
2018-06-01 16:00:27 -07:00
Tim Abbott ad4617c953 push_to_pull_request: Fix handling of .git.
This was throwing the "you can't access the repo" error for this
reason.
2018-06-01 16:00:27 -07:00
Greg Price 5e89c33e7f tools: Add push-to-pull-request tool.
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. :)
2018-05-22 18:33:51 -07:00