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 /doc/stdlib | |
| 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
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 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 |