aboutsummaryrefslogtreecommitdiff
path: root/test-suite/misc
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-03-03 21:52:11 +0000
committerGitHub2021-03-03 21:52:11 +0000
commitbb4e1a76802a5440605264320ed528331ec0e2b7 (patch)
treea4ee40409c92afc6e563cac698e4ed08713cf051 /test-suite/misc
parenta5bea627d1fe742229497b466ca24b470c20d269 (diff)
parentab98d847d237af3cd0e46edef42218be65cfc98f (diff)
Merge PR #12567: [build] Split stdlib to it's own package.
Reviewed-by: Zimmi48 Ack-by: JasonGross Ack-by: gares Ack-by: LasseBlaauwbroek Ack-by: silene Ack-by: vbgl
Diffstat (limited to 'test-suite/misc')
-rwxr-xr-xtest-suite/misc/coq_environment.sh2
1 files changed, 1 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`