diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-06-26 17:37:29 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-06-26 17:37:29 +0200 |
| commit | cda7b80182b03c7b04baf5cc2cc6aa33984e054a (patch) | |
| tree | 75b1be4215f786ab56c3fcc6184b46867444d0f7 /doc/stdlib | |
| parent | f27134ab2cf4fa1ddc1dd19b2b961e3c3ed040ff (diff) | |
Avoid scanning .coq-native directories when building the library index.
Diffstat (limited to 'doc/stdlib')
| -rwxr-xr-x | doc/stdlib/make-library-index | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index 1a70567f6..43802efa0 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 |