# HG changeset patch
# User wenzelm
# Date 1720007688 -7200
# Node ID e0568c7b5bedba7cbfbca51c995776f8a6fbcfc8
# Parent  8a653e8355cc1c79609632a54be48d4b432572e8
unused;

diff -r 8a653e8355cc -r e0568c7b5bed src/Pure/Tools/dump.scala
--- 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))
   }