diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 418289a52bd2..7c6953197c0d 100644
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -12,9 +12,15 @@ if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 # CompCert does compile with -native-compiler yes
 # but with excessive memory requirements
 export COQCOPTS='-native-compiler no -w -undeclared-scope -w -omega-is-deprecated'
-( cd "${CI_BUILD_DIR}/compcert"
-  [ -e Makefile.config ] || ./configure -ignore-coq-version x86_32-linux -install-coqdev -clightgen -use-external-MenhirLib -use-external-Flocq -prefix ${CI_INSTALL_DIR} -coqdevdir ${CI_INSTALL_DIR}/lib/coq/user-contrib/compcert
-  make
-  make check-proof COQCHK='"$(COQBIN)coqchk" -silent -o $(COQINCLUDES)'
-  make install
+(
+	cd "${CI_BUILD_DIR}/compcert"
+	if ! [ -e Makefile.config ]; then
+		./configure -ignore-coq-version x86_32-linux -install-coqdev \
+		-clightgen -use-external-MenhirLib -use-external-Flocq \
+		-prefix "$COQBIN" \
+		-coqdevdir "$COQLIB"/user-contrib/compcert
+	fi
+	make
+	make check-proof COQCHK='"$(COQBIN)coqchk" -silent -o $(COQINCLUDES)'
+	make install
 )