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) }