diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-09 14:16:52 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-09 14:16:52 +0200 |
| commit | 6083ca1d7e654041861ffcd9a835b453717f637f (patch) | |
| tree | 50a9c5e27854121968bb3f27b35ef1f4dcedda48 /dev | |
| parent | fe3977512f18c269e82765995ee1e9ba5d6e4b43 (diff) | |
Merge script: adds a way for confirmation to expect a newline.
This fulfils Gaetan's wish.
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/tools/merge-pr.sh | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 60e3d739c..1c94f630f 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -10,6 +10,14 @@ OFFICIAL_REMOTE_HTTPS_URL="https://github.com/coq/coq" # This script depends (at least) on git (>= 2.7) and jq. # It should be used like this: dev/tools/merge-pr.sh /PR number/ +# Set SLOW_CONF to have the confirmation output wait for a newline +# E.g. call $ SLOW_CONF= dev/tools/merge-pr.sh /PR number/ +if [ -z ${SLOW_CONF+x} ]; then + QUICK_CONF="-n 1" +else + QUICK_CONF="" +fi + RED="\033[31m" RESET="\033[0m" GREEN="\033[32m" @@ -33,7 +41,7 @@ fi } ask_confirmation() { - read -p "Continue anyway? [y/N] " -n 1 -r + read -p "Continue anyway? [y/N] " $QUICK_CONF -r echo if [[ ! $REPLY =~ ^[Yy]$ ]] then |