# HG changeset patch # User wenzelm # Date 1477147167 -7200 # Node ID b89c29ea208f8a64c8b21c69c7973b30026e5da1 # Parent c1695143de355879c493d9fbd3f920f6006f978c permissive rename operation (amending b265dd04d57d); diff -r c1695143de35 -r b89c29ea208f src/Pure/General/file.scala --- a/src/Pure/General/file.scala Sat Oct 22 13:41:18 2016 +0200 +++ b/src/Pure/General/file.scala Sat Oct 22 16:39:27 2016 +0200 @@ -220,13 +220,13 @@ def write_backup(path: Path, text: CharSequence) { - mv(path, path.backup) + if (path.is_file) mv(path, path.backup) write(path, text) } def write_backup2(path: Path, text: CharSequence) { - mv(path, path.backup2) + if (path.is_file) mv(path, path.backup2) write(path, text) }