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

---
 tools/CoqMakefile.in | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'tools')

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