unused;

--- a/src/Pure/Tools/dump.scala	Wed Jul 03 10:16:39 2024 +0200
+++ b/src/Pure/Tools/dump.scala	Wed Jul 03 13:54:48 2024 +0200
@@ -29,9 +29,6 @@
     def write(file_name: Path, bytes: Bytes): Unit =
       Bytes.write(write_path(file_name), bytes)
 
-    def write(file_name: Path, text: String): Unit =
-      write(file_name, Bytes(text))
-
     def write(file_name: Path, body: XML.Body): Unit =
       write(file_name, YXML.bytes_of_body(body, recode = Symbol.encode))
   }