--- a/lib/scripts/fixdots.pl Fri Oct 10 17:10:12 1997 +0200
+++ b/lib/scripts/fixdots.pl Fri Oct 10 17:38:50 1997 +0200
@@ -21,9 +21,9 @@
while (1) {
$_ = $rest;
($pre, $str, $rest) =
- m/^((?: \(\*.*?\*\) | [^"] )*) # pre: text or (non-nested!) comments
+ m/^((?: \(\*.*?\*\) | [^"] )*) # pre: text or (non-nested!) comments
"((?: [^"\\] | \\\S | \\\s+\\ )*)" # quoted string
- (.*)$/sx; # rest of file
+ (.*)$/sx; # rest of file
if ($str) {
$_ = $str;
if (!m/^[a-zA-Z0-9_\/\.]*$/s && !m/\.ML/s && !m/\.thy/s) { # exclude filenames!