tuned \s pattern;
authorwenzelm
Thu, 18 Jun 1998 18:31:06 +0200
changeset 5051 3b45aee5c7ec
parent 5050 e925308df78b
child 5052 bbe3584b515b
tuned \s pattern;
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 = $_;