proper "~~" backup as documented;
authorwenzelm
Fri, 21 Apr 2017 16:48:12 +0200
changeset 65537 7ce5fcebfb35
parent 65536 23c2450ae027
child 65538 a39ef48fbee0
proper "~~" backup as documented;
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)
     }
   }