src/Pure/General/file.scala
changeset 64345 b89c29ea208f
parent 64304 96bc94c87a81
child 64482 43f6c28ff496
--- 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)
   }