# HG changeset patch # User wenzelm # Date 876497930 -7200 # Node ID a162775229287b1cf0a338d04908c25b5f08edcb # Parent d7f033c74b38ede018101970b17b531b79112682 tuned; diff -r d7f033c74b38 -r a16277522928 lib/scripts/fixdots.pl --- 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!