From f8690d31f74f18ac1dd03d0b0922d2908b9c6807 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 4 Apr 2019 14:34:53 +0200
Subject: coq_makefile install target: error if any file is missing

---
 test-suite/coq-makefile/missing-install/run.sh | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100755 test-suite/coq-makefile/missing-install/run.sh

(limited to 'test-suite')

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
-- 
cgit v1.2.3