# HG changeset patch
# User wenzelm
# Date 1646333460 -3600
# Node ID 31c5a22d50ef8d6fcc3ec2018d5d03d9474bccd3
# Parent  6087947afd0ad12fb586db46755270cb6473cb8c
proper init of non-existing file;

diff -r 6087947afd0a -r 31c5a22d50ef src/Pure/General/file.scala
--- 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)