# HG changeset patch
# User wenzelm
# Date 1660312642 -7200
# Node ID 6eb8d6cdb6864ea05d3f065a2eff4fa9a95de92a
# Parent  0a14663dffcccffc0efeda28fe0fca77f2acb33f
proper toString for Content_XML, which is not covered by trait Content;

diff -r 0a14663dffcc -r 6eb8d6cdb686 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Fri Aug 12 15:48:47 2022 +0200
+++ b/src/Pure/General/file.scala	Fri Aug 12 15:57:22 2022 +0200
@@ -330,6 +330,8 @@
   }
 
   final class Content_XML private[File](val path: Path, val content: XML.Body) {
+    override def toString: String = path.toString
+
     def output(out: XML.Body => String): Content_String =
       new Content_String(path, out(content))
   }