From 9152b813eaf000226190f13d69685fbe67b1c96d Mon Sep 17 00:00:00 2001
From: charguer
Date: Fri, 25 Oct 2019 14:30:21 +0200
Subject: fix installation of vos files in coq Makefile

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

(limited to 'tools')

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index b8930997a4..abfbd66e28 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -246,8 +246,10 @@ strip_dotslash = $(patsubst ./%,%,$(1))
 with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1)))
 
 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)
@@ -298,6 +300,7 @@ ALLNATIVEFILES = \
 NATIVEFILES = $(wildcard $(ALLNATIVEFILES))
 FILESTOINSTALL = \
 	$(VOFILES) \
+	$(VOSFILES) \
 	$(VFILES) \
 	$(GLOBFILES) \
 	$(NATIVEFILES) \
-- 
cgit v1.2.3