# HG changeset patch
# User wenzelm
# Date 1456667318 -3600
# Node ID 94f457bea7c1196f78887a518d789fb4379f9212
# Parent  133f65ac17e590960ca42c8f329b0c6f45eea90d
tuned;

diff -r 133f65ac17e5 -r 94f457bea7c1 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sun Feb 28 14:33:53 2016 +0100
+++ b/src/Pure/General/file.scala	Sun Feb 28 14:48:38 2016 +0100
@@ -196,13 +196,13 @@
   def write_backup(path: Path, text: CharSequence)
   {
     path.file renameTo path.backup.file
-    File.write(path, text)
+    write(path, text)
   }
 
   def write_backup2(path: Path, text: CharSequence)
   {
     path.file renameTo path.backup2.file
-    File.write(path, text)
+    write(path, text)
   }