| 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)