# HG changeset patch
# User wenzelm
# Date 1620214050 -7200
# Node ID 27659455c592647e9ee498ea5a3869fe52ff26a7
# Parent  0732f66ce514c5d24cfe68140bcfa3f41003e476
clarified signature;

diff -r 0732f66ce514 -r 27659455c592 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Tue May 04 20:40:09 2021 +0200
+++ b/src/Pure/General/file.scala	Wed May 05 13:27:30 2021 +0200
@@ -279,14 +279,20 @@
 
   /* change */
 
-  def change(file: JFile, f: String => String): Unit = write(file, f(read(file)))
-  def change(path: Path, f: String => String): Unit = write(path, f(read(path)))
+  def change(file: JFile, f: String => String): Unit =
+  {
+    val x = read(file)
+    val y = f(x)
+    if (x != y) write(file, y)
+  }
+
+  def change(path: Path, f: String => String): Unit = change(path.file, f)
 
 
   /* append */
 
   def append(file: JFile, text: String): Unit =
-    Files.write(file.toPath, UTF8.bytes(text.toString),
+    Files.write(file.toPath, UTF8.bytes(text),
       StandardOpenOption.APPEND, StandardOpenOption.CREATE)
 
   def append(path: Path, text: String): Unit = append(path.file, text)