diff --git a/buildjob b/buildjob
index 8f8a8e0249c2d5c8babfbafed6a501eaf1e2397f..eb0917994c8d18772fd82824de8239fc4527ae7f 100755
--- a/buildjob
+++ b/buildjob
@@ -26,6 +26,12 @@ set -o pipefail
 . ci/prepare-opam.sh $OPAM_PINS # deliberately not quoted
 env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt
 
+# maybe set some coq flags
+if [[ -n "$MANGLE_NAMES" ]]; then
+    PREFIX=$(cat /dev/urandom | tr -dc 'a-z' | fold -w 12 | head -n 1)
+    export COQEXTRAFLAGS="$COQEXTRAFLAGS -mangle-names mangled_$PREFIX_"
+fi
+
 # Build
 echo_color "$BOLDGREEN" "[buildjob] Perfoming build"
 time make --output-sync --no-print-directory -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt