diff options
| author | notin | 2008-02-13 14:23:23 +0000 |
|---|---|---|
| committer | notin | 2008-02-13 14:23:23 +0000 |
| commit | 8c7d9c49e34ec0ba22f0e4c34c46b1bf36788308 (patch) | |
| tree | 9a6c16bbfb8c50254ebdad687240ede743cfb511 /doc/Makefile | |
| parent | 5b5e0694d6e55b07c38e9d654206aef2b0964ea5 (diff) | |
Suppression de l'option -glob-from de Coqdoc: les globalisations sont
lues directement des fichiers .glob
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10559 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/Makefile')
| -rw-r--r-- | doc/Makefile | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/doc/Makefile b/doc/Makefile index b6290ff0cb..6e606ed194 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -214,8 +214,6 @@ faq/html/index.html: faq/FAQ.v.html # Standard library ###################################################################### -GLOBDUMP=$(COQSRC)/glob.dump - LIBDIRS= Init Logic Bool Arith NArith ZArith QArith Relations Sets Setoids Lists Sorting Wellfounded IntMap FSets Reals Program # We avoid Strings as String.v contains unicode caracters that make latex fail @@ -229,14 +227,11 @@ ALLTHEORIES_GLOB = $(ALLTHEORIES_V:%.v=%.glob) ### Standard library (browsable html format) -$(GLOBDUMP): $(ALLTHEORIES_GLOB) - $(MAKE) -C .. $(@:../%=%) - -stdlib/index-body.html: $(GLOBDUMP) $(ALLTHEORIES_V) +stdlib/index-body.html: $(ALLTHEORIES_V) - rm -rf stdlib/html mkdir stdlib/html (cd stdlib/html;\ - $(COQDOC) -q --multi-index --html --glob-from $(GLOBDUMP)\ + $(COQDOC) -q --multi-index --html \ -R $(COQSRC)/theories Coq $(ALLTHEORIES_V)) mv stdlib/html/index.html stdlib/index-body.html |