aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/Makefile7
-rwxr-xr-xdoc/Tutorial.tex2
2 files changed, 5 insertions, 4 deletions
diff --git a/doc/Makefile b/doc/Makefile
index cb85f3322c..23617571b7 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -16,7 +16,8 @@
DOCCOQTOP=$(COQBIN)/coqtop.byte
DOCCOQC=$(COQBIN)/coqc
COQTEX=$(COQBIN)/coq-tex -image $(DOCCOQTOP) -v -sl -small
-COQWEBSTY=$(HOME)/tex/inputs
+#COQWEBSTY=$(HOME)/lib/tex/
+COQWEBSTY=/usr/share/texmf/tex/latex/misc/
LATEX=latex
BIBTEX=bibtex
@@ -48,7 +49,7 @@ REFMANFILES= Reference-Manual.tex RefMan-pre.tex RefMan-int.tex \
REFMAN=Reference-Manual
-#VERSION=V7.1
+#VERSION=V7.2
VERSION=POSITIONNEZ-CETTE-VARIABLE
FTPDOCDIR=/net/pauillac/infosystems/ftp/coq/coq/$(VERSION)/doc
WWWDOCDIR=/net/pauillac/infosystems/www/coq/doc
@@ -328,7 +329,7 @@ doc-ftp-www-install: doc-ftp-install doc-www-install
doc-ftp-install:
- mkdir $(FTPDOCDIR)
cp $(FTPDOCS) $(FTPHTMLDOCS) $(FTPDOCDIR)
- chmod g+w $(FTPDOCDIR)/*
+ - chmod g+w $(FTPDOCDIR)/*
doc-www-install:
(cd $(WWWDOCDIR); rm -f node*.html main*.html toc.html \
diff --git a/doc/Tutorial.tex b/doc/Tutorial.tex
index fc22b89bf2..7de9ad9168 100755
--- a/doc/Tutorial.tex
+++ b/doc/Tutorial.tex
@@ -46,7 +46,7 @@ The standard invocation of \Coq\ delivers a message such as:
\begin{flushleft}
\begin{verbatim}
unix:~> coqtop
-Welcome to Coq 7.2 (December 2001)
+Welcome to Coq 7.2 (January 2002)
Coq <
\end{verbatim}