# HG changeset patch
# User wenzelm
# Date 1492786092 -7200
# Node ID 7ce5fcebfb35cbe1cf4d4d691b2ee0a903d3227f
# Parent  23c2450ae02756c27f5528f2a6f7e78a0c2d4d84
proper "~~" backup as documented;

diff -r 23c2450ae027 -r 7ce5fcebfb35 src/Pure/Tools/update_imports.scala
--- a/src/Pure/Tools/update_imports.scala	Fri Apr 21 16:45:32 2017 +0200
+++ b/src/Pure/Tools/update_imports.scala	Fri Apr 21 16:48:12 2017 +0200
@@ -138,7 +138,7 @@
             case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
           }
         })
-      File.write_backup(Path.explode(File.standard_path(file)), new_text)
+      File.write_backup2(Path.explode(File.standard_path(file)), new_text)
     }
   }