diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
| commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
| tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /doc/stdlib/make-library-files | |
| parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) | |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'doc/stdlib/make-library-files')
| -rwxr-xr-x | doc/stdlib/make-library-files | 36 |
1 files changed, 0 insertions, 36 deletions
diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files deleted file mode 100755 index c071c4a2..00000000 --- a/doc/stdlib/make-library-files +++ /dev/null @@ -1,36 +0,0 @@ -#!/bin/sh - -# Needs COQSRC and GALLINA set - -# On garde la liste de tous les *.v avec dates dans library.files.ls -# Si elle a change depuis la derniere fois ou library.files n'existe pas -# on fabrique des .g (si besoin) et la liste library.files dans -# l'ordre de ls -tr des *.vo -# Ce dernier trie les fichiers dans l'ordre inverse de leur date de création -# En supposant que make fait son boulot, ca fait un tri topologique du -# graphe des dépendances - -LIBDIRS="Arith PArith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes Numbers" - -rm -f library.files.ls.tmp -(cd $COQSRC/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp -if ! test -e library.files || ! cmp library.files.ls library.files.ls.tmp; then - mv -f library.files.ls.tmp library.files.ls - rm -f library.files; touch library.files - ABSOLUTE=`pwd`/library.files - cd $COQSRC/theories - echo $LIBDIRS - for rep in $LIBDIRS ; do - (cd $rep - echo $rep/intro.tex >> $ABSOLUTE - VOFILES=`ls -tr *.vo` - for file in $VOFILES ; do - VF=`basename $file \.vo` - if [ \( ! -e $VF.g \) -o \( $VF.v -nt $VF.g \) ] ; then - $GALLINA $VF.v - fi - echo $rep/$VF.g >> $ABSOLUTE - done - ) - done -fi |