From 5bf25dfce23da1cee04b1c886e026f0dbc902c9c Mon Sep 17 00:00:00 2001
From: charguer
Date: Fri, 8 Nov 2019 11:06:10 +0100
Subject: From CoqIDE or -vos or -vok compilation, load .vo when .vos is
 missing (fixing bug #11057). With this new behavior, it is not needed to .vos
 files in user contribs. Also, this commit adds a feature: upon creation of a
 .vo file, an empty .vok file is touched.

---
 tools/CoqMakefile.in | 2 --
 1 file changed, 2 deletions(-)

(limited to 'tools')

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index abfbd66e28..23b9b0bb70 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -249,7 +249,6 @@ VO = vo
 VOS = vos
 
 VOFILES = $(VFILES:.v=.$(VO))
-VOSFILES = $(VFILES:.v=.$(VOS))
 GLOBFILES = $(VFILES:.v=.glob)
 HTMLFILES = $(VFILES:.v=.html)
 GHTMLFILES = $(VFILES:.v=.g.html)
@@ -300,7 +299,6 @@ ALLNATIVEFILES = \
 NATIVEFILES = $(wildcard $(ALLNATIVEFILES))
 FILESTOINSTALL = \
 	$(VOFILES) \
-	$(VOSFILES) \
 	$(VFILES) \
 	$(GLOBFILES) \
 	$(NATIVEFILES) \
-- 
cgit v1.2.3