diff --git a/buildjob b/buildjob index eb0917994c8d18772fd82824de8239fc4527ae7f..b5897aaf1732bedc650b75d05b753db6214a524b 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