author | wenzelm |
Fri, 21 Apr 2017 16:48:12 +0200 | |
changeset 65537 | 7ce5fcebfb35 |
parent 65536 | 23c2450ae027 |
child 65538 | a39ef48fbee0 |
--- 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) } }