diff options
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Makefile.doc b/Makefile.doc index 3822fc7fb9..765aa18454 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -116,10 +116,10 @@ doc/refman-quick: doc/tutorial/Tutorial.v.dvi: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex (cd doc/tutorial; $(LATEX) Tutorial.v) -doc/tutorial/Tutorial.v.pdf: doc/common/version.tex doc/common/title.tex doc/tutorial/Tutorial.v.dvi +doc/tutorial/Tutorial.v.pdf: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex (cd doc/tutorial; $(PDFLATEX) Tutorial.v.tex) -doc/tutorial/Tutorial.v.html: doc/tutorial/Tutorial.v.tex +doc/tutorial/Tutorial.v.html: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex (cd doc/tutorial; hevea -exec xxdate.exe Tutorial.v) @@ -205,7 +205,7 @@ doc/RecTutorial/RecTutorial.v.html: doc/RecTutorial/RecTutorial.v.tex # Not robust, improve... ide/index_urls.txt: doc/refman/html/index.html - rm ide/index_urls.txt - cat doc/refman/html/command-index.html doc/refman/html/tactic-index.html | grep li-itemize | grep HREF | sed -e 's@.*<TT>\(.*\)</TT>.*, <A HREF="\(.*\)">.*@\1,\2@' > ide/index_urls.txt + cat doc/refman/html/command-index.html doc/refman/html/tactic-index.html | grep li-indexenv | grep HREF | sed -e 's@.*<TT>\(.*\)</TT>.*, <A HREF="\(.*\)">.*@\1,\2@' > ide/index_urls.txt ###################################################################### |