# 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)
   }