aboutsummaryrefslogtreecommitdiff
path: root/test-suite/misc
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/misc')
-rwxr-xr-xtest-suite/misc/coq_environment.sh2
-rwxr-xr-xtest-suite/misc/coqtop_print-mod-uid.sh6
2 files changed, 7 insertions, 1 deletions
diff --git a/test-suite/misc/coq_environment.sh b/test-suite/misc/coq_environment.sh
index 667d11f89e..6f7b11c8f1 100755
--- a/test-suite/misc/coq_environment.sh
+++ b/test-suite/misc/coq_environment.sh
@@ -16,7 +16,7 @@ EOT
cp $BIN/coqc .
cp $BIN/coq_makefile .
mkdir -p overridden/tools/
-cp $COQLIB/tools/CoqMakefile.in overridden/tools/
+cp $COQLIB/tools/CoqMakefile.in overridden/tools/ || cp $COQLIB/../coq-core/tools/CoqMakefile.in overridden/tools/
unset COQLIB
N=`./coqc -config | grep COQLIB | grep /overridden | wc -l`
diff --git a/test-suite/misc/coqtop_print-mod-uid.sh b/test-suite/misc/coqtop_print-mod-uid.sh
new file mode 100755
index 0000000000..db1df4bb4b
--- /dev/null
+++ b/test-suite/misc/coqtop_print-mod-uid.sh
@@ -0,0 +1,6 @@
+#!/usr/bin/env bash
+
+export COQBIN=$BIN
+export PATH=$COQBIN:$PATH
+
+[ "$(coqtop -print-mod-uid prerequisite/admit.vo)" = "prerequisite/.coq-native/NTestSuite_admit" ]