From fc6f49563036007e9bd108b3cdfe8f71b1bee4c1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Thu, 19 Apr 2018 13:23:42 +0200
Subject: [PATCH] support -mangle-names flag

---
 buildjob | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/buildjob b/buildjob
index 8f8a8e0..eb09179 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
-- 
GitLab