# HG changeset patch
# User wenzelm
# Date 1547242504 -3600
# Node ID 95dc926fa39c7b981801d65815ea75b1fda097db
# Parent  70f1994988d4a6cf4b911e45b416d321f738f438
clarified output (again);

diff -r 70f1994988d4 -r 95dc926fa39c src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Jan 11 22:34:28 2019 +0100
+++ b/src/Pure/Thy/export.scala	Fri Jan 11 22:35:04 2019 +0100
@@ -82,7 +82,7 @@
     name: String,
     body: Future[(Boolean, Bytes)])
   {
-    override def toString: String = uncompressed().toString
+    override def toString: String = name
 
     val name_elems: List[String] = explode_name(name)