diff options
| author | charguer | 2019-10-25 14:30:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-11-01 12:17:07 +0100 |
| commit | 9152b813eaf000226190f13d69685fbe67b1c96d (patch) | |
| tree | 4735cd3de4f66b67cb461a84bf1ed7dde6d15d99 /tools | |
| parent | 667dc05ce35d45303662598f1e6b1923631431f4 (diff) | |
fix installation of vos files in coq Makefile
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 3 |
1 files changed, 3 insertions, 0 deletions
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) \ |