diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-25 13:22:34 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-25 13:22:34 +0000 |
| commit | dc8d33f4d3c010c657e61ba3e6b31d0e9d666f51 (patch) | |
| tree | bf46290e66700623da243acb7b9be3337e459c49 | |
| parent | ebcb2063bba0f87ef146b20357a4866fe8d0d4b0 (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
| -rw-r--r-- | doc/Makefile | 4 | ||||
| -rwxr-xr-x | doc/stdlib/make-library-index | 7 |
2 files changed, 7 insertions, 4 deletions
diff --git a/doc/Makefile b/doc/Makefile index e4b7e2fe9..d1998d4b1 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 $^ > $@ diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index 1da642df3..ddbcd09fd 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -6,7 +6,10 @@ FILE=$1 cp -f $FILE.template tmp echo -n Building file index-list.prehtml ... -for i in $COQTOP/theories/*; do + +for i in ../theories/*; do + echo $i + d=`basename $i` if [ "$d" != "Num" -a "$d" != "CVS" ]; then for j in $i/*.v; do @@ -15,7 +18,7 @@ for i in $COQTOP/theories/*; do grep -q theories/$d/$b.v tmp a=$? if [ $a = 0 ]; then - sed -e "s/theories\/$d\/$b.v/<a href=\"Coq.$d.$b.html\">$b<\/a>/g" tmp > tmp2 + sed -e "s:theories/$d/$b.v:<a href=\"Coq.$d.$b.html\">$b</a>:g" tmp > tmp2 mv -f tmp2 tmp else echo Warning: theories/$d/$b.v is missing in the template file |