permissive rename operation (amending b265dd04d57d);

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