lib/scripts/fixgoal.pl

--- a/lib/scripts/fixgoal.pl	Thu Jun 18 18:28:45 1998 +0200
+++ b/lib/scripts/fixgoal.pl	Thu Jun 18 18:31:06 1998 +0200
@@ -11,15 +11,14 @@
     undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
     close FILE || die $!;
 
-    $thy = "";
     ($path, $thy, $ext) = ($file =~ m,^(.*/)?(\w+)(\.\w+)?$,);
 
     $_ = $text;
 
-    s/^\s*goalw\b\s*\bthy\b/Goalw/mg;
-    s/^\s*goalw\b\s*\b$thy\.thy\b/Goalw/mg;
-    s/^\s*goal\b\s*\bthy\b/Goal/mg;
-    s/^\s*goal\b\s*\b$thy\.thy\b/Goal/mg;
+    s/^[ \t]*goalw\b\s*\bthy\b/Goalw/mg;
+    s/^[ \t]*goalw\b\s*\b$thy\.thy\b/Goalw/mg;
+    s/^[ \t]*goal\b\s*\bthy\b/Goal/mg;
+    s/^[ \t]*goal\b\s*\b$thy\.thy\b/Goal/mg;
 
 
     $result = $_;