diff options
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.doc b/Makefile.doc index 59382b9de..7b8ade09e 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -116,7 +116,7 @@ doc/refman/Reference-Manual.html: doc/refman/styles.hva doc/refman/headers.hva d (cd doc/refman; BIBINPUTS=.: $(HEVEA) $(HEVEAOPTS) ./styles.hva ./Reference-Manual.tex) doc/refman/cover.html: doc/common/styles/html/$(HTMLSTYLE)/cover.html - $(INSTALLLIB) $< doc/refman + sed -e "s/COQVERSION/$(VERSION)/g" $< > $@ doc/refman/styles.hva: doc/common/styles/html/$(HTMLSTYLE)/styles.hva $(INSTALLLIB) $< doc/refman |