diff -r 8a467dc6e667 -r 8315021bf7d6 lib/scripts/fixdots.pl
--- a/lib/scripts/fixdots.pl	Mon Nov 03 11:48:02 1997 +0100
+++ b/lib/scripts/fixdots.pl	Mon Nov 03 11:48:29 1997 +0100
@@ -38,7 +38,9 @@
 
     if ($text ne $result) {
 	print STDERR "fixing $file\n";
-	rename $file, "$file~~" || die $!;
+        if (! -f "$file~~") {
+	    rename $file, "$file~~" || die $!;
+        }
 	open (FILE, "> $file") || die $!;
 	print FILE $result;
 	close FILE || die $!;