summaryrefslogtreecommitdiff
path: root/doc/stdlib/make-library-index
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
commit7cfc4e5146be5666419451bdd516f1f3f264d24a (patch)
treee4197645da03dc3c7cc84e434cc31d0a0cca7056 /doc/stdlib/make-library-index
parent420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff)
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'doc/stdlib/make-library-index')
-rwxr-xr-xdoc/stdlib/make-library-index8
1 files changed, 2 insertions, 6 deletions
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
index 1a70567f..43802efa 100755
--- a/doc/stdlib/make-library-index
+++ b/doc/stdlib/make-library-index
@@ -6,17 +6,14 @@ FILE=$1
HIDDEN=$2
cp -f $FILE.template tmp
-echo -n Building file index-list.prehtml ...
+echo -n "Building file index-list.prehtml... "
#LIBDIRS="Init Logic Structures Bool Arith PArith NArith ZArith QArith Relations Sets Classes Setoids Lists Vectors Sorting Wellfounded MSets FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings"
-LIBDIRS=`find theories/* -type d | sed -e "s:^theories/::"`
+LIBDIRS=`find theories/* -type d ! -name .coq-native | sed -e "s:^theories/::"`
for k in $LIBDIRS; do
i=theories/$k
- echo $i
-
d=`basename $i`
- if [ "$d" != "CVS" ]; then
ls $i | grep -q \.v'$'
if [ $? = 0 ]; then
for j in $i/*.v; do
@@ -46,7 +43,6 @@ for k in $LIBDIRS; do
fi
done
fi
- fi
rm -f tmp2
sed -e "s/#$d#//" tmp > tmp2
mv -f tmp2 tmp