# HG changeset patch
# User wenzelm
# Date 1646324004 -3600
# Node ID ee1bd0687c2b8f2c16fa66045d8dbd25e6bb211f
# Parent  4fdde010086f4b69b209bd7e7cb64e69cd176d76
tuned;

diff -r 4fdde010086f -r ee1bd0687c2b src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Thu Mar 03 17:11:43 2022 +0100
+++ b/src/Pure/General/file.scala	Thu Mar 03 17:13:24 2022 +0100
@@ -243,11 +243,13 @@
     if (x != y) write(file, y)
   }
 
+  def change(path: Path)(f: String => String): Unit = change(path.file)(f)
+
   def change_lines(file: JFile)(f: List[String] => List[String]): Unit =
     change(file)(text => cat_lines(f(split_lines(text))))
 
-  def change(path: Path)(f: String => String): Unit = change(path.file)(f)
-  def change_lines(path: Path)(f: List[String] => List[String]): Unit = change_lines(path.file)(f)
+  def change_lines(path: Path)(f: List[String] => List[String]): Unit =
+    change_lines(path.file)(f)
 
 
   /* append */