diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/Makefile b/doc/Makefile index 187c48e4aa..cbaeb8e868 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -51,7 +51,7 @@ REFMANFILES= Reference-Manual.tex RefMan-pre.tex RefMan-int.tex \ REFMAN=Reference-Manual #VERSION=POSITIONNEZ-CETTE-VARIABLE -VERSION=V7.3 +VERSION=V7.4 FTPDOCDIR=/net/pauillac/infosystems/ftp/coq/coq/$(VERSION)/doc WWWDOCDIR=/net/pauillac/infosystems/www/coq/doc |