aboutsummaryrefslogtreecommitdiff
path: root/doc/Makefile
diff options
context:
space:
mode:
authornotin2006-03-25 13:22:34 +0000
committernotin2006-03-25 13:22:34 +0000
commitdc8d33f4d3c010c657e61ba3e6b31d0e9d666f51 (patch)
treebf46290e66700623da243acb7b9be3337e459c49 /doc/Makefile
parentebcb2063bba0f87ef146b20357a4866fe8d0d4b0 (diff)
r8708@thot: notin | 2006-03-24 18:55:01 +0100
Correction d'un bug sur la génération de la doc de stdlib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8662 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/Makefile')
-rw-r--r--doc/Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/Makefile b/doc/Makefile
index e4b7e2fe97..d1998d4b16 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -207,7 +207,7 @@ faq/html/index.html: faq/FAQ.v.html
GLOBDUMP=$(COQTOP)/glob.dump
-LIBDIRS= Logic Bool Arith ZArith Reals Lists Sets Relations Sorting Wellfounded IntMap
+LIBDIRS= Logic Bool Arith ZArith Reals Lists Sets Relations Sorting Wellfounded IntMap FSets
### Standard library (browsable html format)
@@ -220,7 +220,7 @@ stdlib/index-body.html: $(GLOBDUMP)
mv stdlib/html/index.html stdlib/index-body.html
stdlib/index-list.html: stdlib/index-list.html.template
- ./stdlib/make-library-index stdlib/index-list.html
+ COQTOP=$(COQTOP) ./stdlib/make-library-index stdlib/index-list.html
stdlib/html/index.html: stdlib/index-list.html stdlib/index-body.html stdlib/index-trailer.html
cat $^ > $@