aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-04-04 14:34:53 +0200
committerGaëtan Gilbert2019-04-08 13:15:47 +0200
commitf8690d31f74f18ac1dd03d0b0922d2908b9c6807 (patch)
tree5714c5eccb0362c437212cddec36fd2716392a54 /test-suite
parent81df7850d40273814fcf78cf6df9057f19fa9a8e (diff)
coq_makefile install target: error if any file is missing
Diffstat (limited to 'test-suite')
-rwxr-xr-xtest-suite/coq-makefile/missing-install/run.sh17
1 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/coq-makefile/missing-install/run.sh b/test-suite/coq-makefile/missing-install/run.sh
new file mode 100755
index 0000000000..4f36fdcb1c
--- /dev/null
+++ b/test-suite/coq-makefile/missing-install/run.sh
@@ -0,0 +1,17 @@
+#!/usr/bin/env bash
+
+. ../template/init.sh
+
+rm -rf _test; mkdir _test; cd _test
+
+cat > _CoqProject <<EOF
+-R theories Test
+theories/a.v
+theories/b.v
+EOF
+mkdir theories
+touch theories/a.v theories/b.v
+
+coq_makefile -f _CoqProject -o Makefile
+make theories/b.vo
+if make install; then exit 1; fi