4 files changed, 14 insertions, 7 deletions
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index fc3cef3426..7bf2c7427d 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -8,4 +8,5 @@ CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert
 opam install -j ${NJOBS} -y menhir
 git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR}
 
-( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make && make check-proof )
+#( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make && make check-proof )
+( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make )
diff --git a/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh b/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh
new file mode 100644
index 0000000000..cdca8e525a
--- /dev/null
+++ b/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh
@@ -0,0 +1,4 @@
+if [ "$TRAVIS_PULL_REQUEST" = "6158" ] || [ "$TRAVIS_BRANCH" = "master+some-fix-ltac-printing+refined-printers" ]; then
+    ltac2_CI_BRANCH=master+fix-pr6158-ltac-value-printer
+    ltac2_CI_GITURL=https://github.com/herbelin/ltac2.git
+fi
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
index bc6ee31916..4c4dbe1e97 100755
--- a/dev/tools/backport-pr.sh
+++ b/dev/tools/backport-pr.sh
@@ -1,6 +1,6 @@
 #!/usr/bin/env bash
 
-# Usage: git-backport <PR number>
+# Usage: dev/tools/backport-pr.sh <PR number>
 
 set -e
 
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index f770004a5c..0c4a79bfd3 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -1,4 +1,6 @@
-#!/bin/sh -e
+#!/usr/bin/env bash
+
+set -e
 
 # This script depends (at least) on git and jq.
 # It should be used like this: dev/tools/merge-pr.sh /PR number/
@@ -15,12 +17,12 @@ API=https://api.github.com/repos/coq/coq
 
 BASE_BRANCH=`curl -s $API/pulls/$PR | jq -r '.base.label'`
 
-COMMIT=`git rev-parse $REMOTE/pr/$PR`
+COMMIT=`git rev-parse FETCH_HEAD`
 STATUS=`curl -s $API/commits/$COMMIT/status | jq -r '.state'`
 
 if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then
   echo "Wrong base branch"
-  read -p "Bypass? [y/n] " -n 1 -r
+  read -p "Bypass? [y/N] " -n 1 -r
   echo
   if [[ ! $REPLY =~ ^[Yy]$ ]]
   then
@@ -30,7 +32,7 @@ fi;
 
 if [ $STATUS != "success" ]; then
   echo "CI status is \"$STATUS\""
-  read -p "Bypass? [y/n] " -n 1 -r
+  read -p "Bypass? [y/N] " -n 1 -r
   echo
   if [[ ! $REPLY =~ ^[Yy]$ ]]
   then
@@ -38,7 +40,7 @@ if [ $STATUS != "success" ]; then
   fi
 fi;
 
-git merge -S --no-ff $REMOTE/pr/$PR -m "Merge PR #$PR: `curl -s $API/pulls/$PR | jq -r '.title'`" -e
+git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: `curl -s $API/pulls/$PR | jq -r '.title'`" -e
 
 # TODO: improve this check
 if [[ `git diff $REMOTE/$CURRENT_LOCAL_BRANCH dev/ci` ]]; then