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

---
 CHANGES.md                                     |  2 ++
 test-suite/coq-makefile/missing-install/run.sh | 17 +++++++++++++++++
 tools/CoqMakefile.in                           |  3 +++
 3 files changed, 22 insertions(+)
 create mode 100755 test-suite/coq-makefile/missing-install/run.sh

diff --git a/CHANGES.md b/CHANGES.md
index ce8a787cd1..48d5a7af7e 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -227,6 +227,8 @@ Tools
   `coqc`/`make` as well as printing to stdout, on both python2 and
   python3.
 
+- coq_makefile's install target now errors if any file to install is missing.
+
 Standard Library
 
 - Added lemmas about monotonicity of `N.double` and `N.succ_double`, and about
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
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index bd9d8c9221..0236c549d5 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -468,6 +468,9 @@ beautify: $(BEAUTYFILES)
 # Extensions can't assume when they run.
 
 install:
+	$(HIDE)code=0; for f in $(FILESTOINSTALL); do\
+	 if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \
+	done; exit $$code
 	$(HIDE)for f in $(FILESTOINSTALL); do\
 	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
 	 if [ "$$?" != "0" -o -z "$$df" ]; then\
-- 
cgit v1.2.3