# HG changeset patch
# User paulson
# Date 822063622 -3600
# Node ID 887e9816eea468c371050e86d33053ddb84f8306
# Parent  23ceb1dc9755a8ad6f0230697d0cc52f54102bf4
Now expands TABS as well

diff -r 23ceb1dc9755 -r 887e9816eea4 src/Tools/expandshort
--- a/src/Tools/expandshort	Thu Jan 18 10:38:29 1996 +0100
+++ b/src/Tools/expandshort	Fri Jan 19 16:00:22 1996 +0100
@@ -3,6 +3,7 @@
 #Shell script to expand shorthand goal commands
 #  ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
 #     rewrite_goals_tac on 1-element lists
+#  ALSO expands tabs, since they are now forbidden in strings.
 #
 # Usage:
 #    expandshort FILE1 ... FILEn
@@ -26,6 +27,6 @@
 s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g
 s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g
 s/rewrite_goals_tac *\[\([a-zA-Z0-9_]*\)\]\( *\)/rewtac \1\2/g
-' $f~~ > $f
+' $f~~ | expand > $f
 done
 echo Finished.