author | wenzelm |
Thu, 03 Mar 2022 19:51:00 +0100 | |
changeset 75208 | 31c5a22d50ef |
parent 75207 | 6087947afd0a |
child 75209 | 4187f6f18232 |
--- a/src/Pure/General/file.scala Thu Mar 03 19:50:41 2022 +0100 +++ b/src/Pure/General/file.scala Thu Mar 03 19:51:00 2022 +0100 @@ -247,7 +247,7 @@ def change(path: Path, init: Boolean = false)(f: String => String): Unit = { - if (init) append(path, "") + if (!path.is_file && init) write(path, "") val x = read(path) val y = f(x) if (x != y) write(path, y)