diff options
| author | Emilio Jesus Gallego Arias | 2019-02-21 03:44:32 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-21 03:44:32 +0100 |
| commit | a34bc49621456cfd11ead110164747862b50f247 (patch) | |
| tree | 6d318df5a2dd923857dc6102f8492d2891e20842 /dev/tools | |
| parent | 924468eb648750bf2cbb6de0b1c8f7a2960f0bf5 (diff) | |
| parent | 5664f0a67d17f9e5717ded6afbda70b36ea8c9f3 (diff) | |
Merge PR #9388: merge-pr.sh: fix #9387: quick_conf doesn't work in emacs shell buffer
Reviewed-by: ejgallego
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/merge-pr.sh | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 813ad71be9..425f21de70 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -12,7 +12,8 @@ OFFICIAL_REMOTE_HTTPS_URL="github.com/coq/coq" # 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 +# emacs doesn't send characters until the RET so we can't quick_conf +if [ -z ${SLOW_CONF+x} ] || [ -n "$INSIDE_EMACS" ]; then QUICK_CONF="-n 1" else QUICK_CONF="" |