| changeset 4076 | 8315021bf7d6 |
| parent 3838 | a16277522928 |
| child 9789 | 7e5e6c47c0b5 |
--- 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 $!;