diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-23 14:21:14 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-23 14:21:14 +0000 |
commit | 015781acfe4a2a75eeced513528b389cae9fb0a3 (patch) | |
tree | 1b0268353d7e1b589a3619f6ea4ba4ac58b6f473 /doc/stdlib/make-library-index | |
parent | 6cf8d80ac0a9869d97373d6813441eabebce8980 (diff) |
Mise à jour des Makefile, ajout licences, corrections mineures suite à
restructuration du répertoire de documentation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8607 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/stdlib/make-library-index')
-rwxr-xr-x | doc/stdlib/make-library-index | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index new file mode 100755 index 000000000..1da642df3 --- /dev/null +++ b/doc/stdlib/make-library-index @@ -0,0 +1,32 @@ +#!/bin/sh + +# Instantiate links to library files in index template + +FILE=$1 + +cp -f $FILE.template tmp +echo -n Building file index-list.prehtml ... +for i in $COQTOP/theories/*; do + d=`basename $i` + if [ "$d" != "Num" -a "$d" != "CVS" ]; then + for j in $i/*.v; do + b=`basename $j .v` + rm -f tmp2 + 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 + mv -f tmp2 tmp + else + echo Warning: theories/$d/$b.v is missing in the template file + fi + done + fi + rm -f tmp2 + sed -e "s/#$d#//" tmp > tmp2 + mv -f tmp2 tmp +done +a=`grep theories tmp` +if [ $? = 0 ]; then echo Warning: extra files:; echo $a; fi +mv tmp $FILE +echo Done |