changeset 69635 | 95dc926fa39c |
parent 69634 | 70f1994988d4 |
child 69671 | 2486792eaf61 |
--- 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)