equal
deleted
inserted
replaced
10 function usage() |
10 function usage() |
11 { |
11 { |
12 echo |
12 echo |
13 echo "Usage: $PRG [FILES ...]" |
13 echo "Usage: $PRG [FILES ...]" |
14 echo |
14 echo |
15 echo "Expand shorthand goal commands in FILES. Also contracts uses of" |
15 echo " Expand shorthand goal commands in FILES. Also contracts uses of" |
16 echo "resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on" |
16 echo " resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on" |
17 echo "1-element lists; furthermore expands tabs, since they are now" |
17 echo " 1-element lists; furthermore expands tabs, since they are now" |
18 echo "forbidden in strings." |
18 echo " forbidden in strings." |
19 echo |
19 echo |
20 echo "Renames old versions of FILES by appending \"~~\"." |
20 echo " Renames old versions of FILES by appending \"~~\"." |
21 echo |
21 echo |
22 exit 1 |
22 exit 1 |
23 } |
23 } |
24 |
24 |
25 function fail() |
25 function fail() |
28 exit 2 |
28 exit 2 |
29 } |
29 } |
30 |
30 |
31 |
31 |
32 ## main |
32 ## main |
|
33 |
|
34 [ "$1" = "-?" ] && usage |
33 |
35 |
34 for f in "$@" |
36 for f in "$@" |
35 do |
37 do |
36 echo Expanding shorthands in $f. \ Backup file is $f~~ |
38 echo Expanding shorthands in $f. \ Backup file is $f~~ |
37 if [ ! -s $f ]; then echo "File $f is EMPTY!!"; exit 1; fi |
39 if [ ! -s $f ]; then echo "File $f is EMPTY!!"; exit 1; fi |