# HG changeset patch
# User paulson
# Date 849022623 -3600
# Node ID d2a9c34845a25e74886cdb790273173d4d25ef55
# Parent  71385461570a31581adaaf87c06087100fff536a
Checks for empty files.  Replaces auto() calls

diff -r 71385461570a -r d2a9c34845a2 src/Tools/expandshort
--- a/src/Tools/expandshort	Tue Nov 26 16:33:59 1996 +0100
+++ b/src/Tools/expandshort	Tue Nov 26 16:37:03 1996 +0100
@@ -13,6 +13,7 @@
 for f in $*
 do
 echo Expanding shorthands in $f. \ Backup file is $f~~
+if [ ! -s $f ]; then echo "File $f is EMPTY!!"; exit 1; fi
 mv $f $f~~; sed -e '
 s/\<by(/by (/
 s/\<ba \([0-9][0-9]*\);/by (assume_tac \1);/
@@ -24,6 +25,7 @@
 s/\<bes \([^;]*\) \([0-9][0-9]*\);/by (eresolve_tac \1 \2);/
 s/\<bw \([^;]*\);/by (rewtac \1);/
 s/\<bws \([^;]*\);/by (rewrite_goals_tac \1);/
+s/\<auto *()/by (Auto_tac())/
 s/dresolve_tac *\[\([a-zA-Z0-9_]*\)\] */dtac \1 /g
 s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g
 s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g