author | wenzelm |
Fri, 11 Jan 2019 22:35:04 +0100 | |
changeset 69635 | 95dc926fa39c |
parent 69634 | 70f1994988d4 |
child 69636 | dd1e0e1570d2 |
--- 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)