6 files changed, 35 insertions, 5 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index f0dbe485f7..c01bc57f72 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -37,17 +37,19 @@ export PATH="$COQBIN:$PATH"
 # Coq's tools need an ending slash :S, we should fix them.
 export COQBIN="$COQBIN/"
 
-ls "$COQBIN"
+ls -l "$COQBIN"
 
 # Where we download and build external developments
 CI_BUILD_DIR="$PWD/_build_ci"
 
+ls -l "$CI_BUILD_DIR" || true
+
+set +x
 for overlay in "${ci_dir}"/user-overlays/*.sh; do
     # shellcheck source=/dev/null
     . "${overlay}"
 done
 
-set +x
 # shellcheck source=ci-basic-overlay.sh
 . "${ci_dir}/ci-basic-overlay.sh"
 set -x
@@ -84,7 +86,7 @@ git_download()
       COMMIT="$REF"
     fi
     wget "$ARCHIVEURL/$COMMIT.tar.gz"
-    tar xvfz "$COMMIT.tar.gz" --strip-components=1
+    tar xfz "$COMMIT.tar.gz" --strip-components=1
     rm -f "$COMMIT.tar.gz"
   fi
 }
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 59a85e4726..9cb7a65ab5 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -6,4 +6,6 @@ ci_dir="$(dirname "$0")"
 git_download compcert
 
 ( cd "${CI_BUILD_DIR}/compcert" && \
-  ./configure -ignore-coq-version x86_32-linux && make && make check-proof )
+      ./configure -ignore-coq-version x86_32-linux && \
+      make && \
+      make check-proof COQCHK='"$(COQBIN)coqchk" -silent -o $(COQINCLUDES)')
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
index 169d1a41db..4a332406a2 100755
--- a/dev/ci/ci-vst.sh
+++ b/dev/ci/ci-vst.sh
@@ -5,4 +5,6 @@ ci_dir="$(dirname "$0")"
 
 git_download vst
 
+export COMPCERT=bundled
+
 ( cd "${CI_BUILD_DIR}/vst" && make IGNORECOQVERSION=true )
diff --git a/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh b/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh
new file mode 100644
index 0000000000..72ec55a37c
--- /dev/null
+++ b/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh
@@ -0,0 +1,18 @@
+if [ "$CI_PULL_REQUEST" = "11836" ] || [ "$CI_BRANCH" = "obligations+functional" ]; then
+
+    mtac2_CI_REF=obligations+functional
+    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+    paramcoq_CI_REF=obligations+functional
+    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+    equations_CI_REF=obligations+functional
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    metacoq_CI_REF=obligations+functional
+    metacoq_CI_GITURL=https://github.com/ejgallego/metacoq
+
+    rewriter_CI_REF=obligations+functional
+    rewriter_CI_GITURL=https://github.com/ejgallego/rewriter
+
+fi
diff --git a/dev/ci/user-overlays/12650-SkySkimmer-rebuild-record.sh b/dev/ci/user-overlays/12650-SkySkimmer-rebuild-record.sh
new file mode 100644
index 0000000000..d4c67b03b5
--- /dev/null
+++ b/dev/ci/user-overlays/12650-SkySkimmer-rebuild-record.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12650" ] || [ "$CI_BRANCH" = "rebuild-record" ]; then
+
+    elpi_CI_REF=rebuild-record
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+fi
diff --git a/dev/tools/make-changelog.sh b/dev/tools/make-changelog.sh
index de58527cca..413433ef41 100755
--- a/dev/tools/make-changelog.sh
+++ b/dev/tools/make-changelog.sh
@@ -28,7 +28,7 @@ esac
 printf "Fixes? (space separated list of bug numbers)\n"
 read -r fixes_list
 
-fixes_string="$(echo $fixes_list | sed 's/ /~  and /g; s,\([0-9]\+\),`#\1 <https://github.com/coq/coq/issues/\1>`_,g' | tr '~' '\n')"
+fixes_string="$(echo $fixes_list | sed 's/ /~  and /g; s,\([0-9][0-9]*\),`#\1 <https://github.com/coq/coq/issues/\1>`_,g' | tr '~' '\n')"
 if [ ! -z "$fixes_string" ]; then fixes_string="$(printf '\n  fixes %s,' "$fixes_string")"; fi
 
 # shellcheck disable=SC2016