Now expands TABS as well
authorpaulson
Fri Jan 19 16:00:22 1996 +0100 (1996-01-19)
changeset 1445887e9816eea4
parent 1444 23ceb1dc9755
child 1446 a8387e934fa7
Now expands TABS as well
src/Tools/expandshort
     1.1 --- a/src/Tools/expandshort	Thu Jan 18 10:38:29 1996 +0100
     1.2 +++ b/src/Tools/expandshort	Fri Jan 19 16:00:22 1996 +0100
     1.3 @@ -3,6 +3,7 @@
     1.4  #Shell script to expand shorthand goal commands
     1.5  #  ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
     1.6  #     rewrite_goals_tac on 1-element lists
     1.7 +#  ALSO expands tabs, since they are now forbidden in strings.
     1.8  #
     1.9  # Usage:
    1.10  #    expandshort FILE1 ... FILEn
    1.11 @@ -26,6 +27,6 @@
    1.12  s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g
    1.13  s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g
    1.14  s/rewrite_goals_tac *\[\([a-zA-Z0-9_]*\)\]\( *\)/rewtac \1\2/g
    1.15 -' $f~~ > $f
    1.16 +' $f~~ | expand > $f
    1.17  done
    1.18  echo Finished.