| author | huffman | 
| Thu, 23 Jun 2005 22:08:24 +0200 | |
| changeset 16554 | 5841e7f9eef5 | 
| parent 15847 | c05c7670f166 | 
| permissions | -rwxr-xr-x | 
| 10555 | 1 | #!/usr/bin/env bash | 
| 4077 | 2 | # | 
| 3 | # $Id$ | |
| 9788 | 4 | # Author: Markus Wenzel, TU Muenchen | 
| 4077 | 5 | # | 
| 6 | # DESCRIPTION: fix references to implicit claset and simpset | |
| 7 | ||
| 8 | ||
| 9 | ## diagnostics | |
| 10 | ||
| 10511 | 11 | PRG="$(basename "$0")" | 
| 4077 | 12 | |
| 13 | function usage() | |
| 14 | {
 | |
| 15 | echo | |
| 16 | echo "Usage: $PRG [FILES|DIRS...]" | |
| 17 | echo | |
| 18 | echo " Recursively find .ML files, fixing references to" | |
| 4130 | 19 | echo " implicit claset and simpset." | 
| 4077 | 20 | echo | 
| 21 | echo " Renames old versions of FILES by appending \"~~\"." | |
| 22 | echo | |
| 23 | exit 1 | |
| 24 | } | |
| 25 | ||
| 26 | ||
| 27 | ## process command line | |
| 28 | ||
| 9788 | 29 | [ "$#" -eq 0 -o "$1" = "-?" ] && usage | 
| 4077 | 30 | |
| 9788 | 31 | SPECS="$@"; shift "$#" | 
| 4077 | 32 | |
| 33 | ||
| 34 | ## main | |
| 35 | ||
| 6082 | 36 | #set by configure | 
| 15847 
c05c7670f166
restored AUTO_BASH/PERL -- beware of ./configure!
 wenzelm parents: 
15574diff
changeset | 37 | AUTO_PERL=perl | 
| 6082 | 38 | |
| 9788 | 39 | find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixclasimp.pl" |