From 7ae823c0e476e9e9c576671ed10bcffbbcba0ec5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Thu, 19 Apr 2018 13:37:31 +0200
Subject: [PATCH] don't try to be quite so clever with mangling

---
 buildjob | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/buildjob b/buildjob
index eb09179..b5897aa 100755
--- a/buildjob
+++ b/buildjob
@@ -28,8 +28,7 @@ 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_"
+    export COQEXTRAFLAGS="$COQEXTRAFLAGS -mangle-names mangled_"
 fi
 
 # Build
-- 
GitLab