# 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!