diff options
Diffstat (limited to 'doc')
| -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 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 $^ > $@ diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index 1da642df31..ddbcd09fdf 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 |