aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/stdlib
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-08-23 12:52:54 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-08-23 12:52:54 +0000
commite7e7a5890bc75572d5d7d4d9d327db157095c170 (patch)
tree727ff582f69624a085addde82240bdb62fb180b8 /doc/stdlib
parent7f11dda679a72f7eccbe4540d269c1218cd48780 (diff)
Remove a script unused since 2006 (cf commit r8626)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15755 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/stdlib')
-rwxr-xr-xdoc/stdlib/make-library-files36
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 0dd4dac06..000000000
--- 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 Vectors"
-
-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