diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-07-04 16:28:00 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-07-04 16:28:00 +0000 |
| commit | 8595d68b5eae53146aa625c793ea3e478f39878a (patch) | |
| tree | 703eb381f4d5497b01d60fda058752e522b7e670 /doc | |
| parent | 56b935fbc379815ad70b46f3f50da55e8427824c (diff) | |
Ajout cible refman-quick qui teste la compilation sans faire les index, toc et biblio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9004 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/Makefile | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/Makefile b/doc/Makefile index 5ae239006..fde250012 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -164,6 +164,12 @@ refman/html/index.html: refman/Reference-Manual.html $(REFMANPNGFILES) \ cp refman/cover.html refman/menu.html refman/html cp refman/index.html refman/html +refman-quick: + (cd refman; \ + $(PDFLATEX) Reference-Manual.tex; \ + hevea -fix -exec xxdate.exe ./Reference-Manual.tex) + + ###################################################################### # Tutorial ###################################################################### |