diff options
Diffstat (limited to 'doc/stdlib')
| -rwxr-xr-x | doc/stdlib/make-library-index | 7 |
1 files changed, 5 insertions, 2 deletions
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 |