equal
deleted
inserted
replaced
1 #! /bin/sh |
1 #! /bin/sh |
2 # |
2 # $Id$ |
3 #expandshort - shell script to expand shorthand goal commands |
3 #Shell script to expand shorthand goal commands |
4 # ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac, |
4 # ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac, |
5 # rewrite_goals_tac on 1-element lists |
5 # rewrite_goals_tac on 1-element lists |
6 # |
6 # |
7 # Usage: |
7 # Usage: |
8 # expandshort FILE1 ... FILEn |
8 # expandshort FILE1 ... FILEn |
9 # |
9 # |
10 # leaves previous versions as XXX~~ |
10 #Renames old versions of the files as FILE1~~ ... FILEn~~ |
11 # |
11 # |
12 for f in $* |
12 for f in $* |
13 do |
13 do |
14 echo Expanding shorthands in $f. \ Backup file is $f~~ |
14 echo Expanding shorthands in $f. \ Backup file is $f~~ |
15 mv $f $f~~; sed -e ' |
15 mv $f $f~~; sed -e ' |