From 26a7b7196cdf5ee64b886adbaed5bc66a61247ee Mon Sep 17 00:00:00 2001
From: Anders Kaseorg <anders@zulip.com>
Date: Fri, 22 Jan 2021 10:47:45 -0800
Subject: [PATCH] push-to-pull-request: Use getopt.

Signed-off-by: Anders Kaseorg <anders@zulip.com>
---
 tools/push-to-pull-request | 24 ++++++++++++++++++++----
 1 file changed, 20 insertions(+), 4 deletions(-)

diff --git a/tools/push-to-pull-request b/tools/push-to-pull-request
index 90a30295a7..f1b312e5c0 100755
--- a/tools/push-to-pull-request
+++ b/tools/push-to-pull-request
@@ -2,8 +2,8 @@
 set -e
 
 usage() {
-    cat >&2 <<EOF
-usage: $0 PULL_REQUEST_ID [REMOTE]
+    cat <<EOF
+usage: $0 [--merge] PULL_REQUEST_ID [REMOTE]
 
 Force-push our HEAD to the given GitHub pull request branch.
 
@@ -22,9 +22,24 @@ branch is updated to reflect the pushed version.
 
 See also \`reset-to-pull-request\`.
 EOF
-    exit 1
 }
 
+args="$(getopt -o '' --long help -n "$0" -- "$@")"
+eval "set -- $args"
+
+while true; do
+    case "$1" in
+        --help)
+            usage
+            exit 0
+            ;;
+        --)
+            shift
+            break
+            ;;
+    esac
+done
+
 remote_default="$(git config zulip.zulipRemote || echo upstream)"
 pseudo_remote="$(git config zulip.prPseudoRemote || echo)"
 
@@ -32,7 +47,8 @@ pr_id="$1"
 remote="${2:-"$remote_default"}"
 
 if [ -z "$pr_id" ]; then
-    usage
+    usage >&2
+    exit 1
 fi
 
 if ! jq --version >/dev/null 2>&1; then