# HG changeset patch
# User wenzelm
# Date 898187466 -7200
# Node ID 3b45aee5c7ecdf4873bfed7f6a2cc476f8167f06
# Parent  e925308df78be48e843a5fe57af7499b441dc5ca
tuned \s pattern;

diff -r e925308df78b -r 3b45aee5c7ec 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 = $_;