summaryrefslogtreecommitdiff
path: root/test-suite/coq-makefile/emptyprefix/run.sh
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/coq-makefile/emptyprefix/run.sh')
-rwxr-xr-xtest-suite/coq-makefile/emptyprefix/run.sh17
1 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/coq-makefile/emptyprefix/run.sh b/test-suite/coq-makefile/emptyprefix/run.sh
new file mode 100755
index 00000000..a10e63b4
--- /dev/null
+++ b/test-suite/coq-makefile/emptyprefix/run.sh
@@ -0,0 +1,17 @@
+#!/usr/bin/env bash
+
+set -e
+
+. ../template/init.sh
+
+mv theories/sub theories2
+
+coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
+make
+
+cp ../_CoqProject.sub theories2/_CoqProject
+cd theories2
+coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
+make