author | wenzelm |
Thu, 04 Mar 2021 16:08:30 +0100 | |
changeset 73363 | 5e312d6bb883 |
parent 73362 | dde25151c3c1 |
child 73364 | 6bf6160a2c54 |
--- a/src/Pure/PIDE/command.scala Thu Mar 04 15:59:28 2021 +0100 +++ b/src/Pure/PIDE/command.scala Thu Mar 04 16:08:30 2021 +0100 @@ -519,7 +519,7 @@ val init_results: Command.Results, val init_markups: Command.Markups) { - override def toString: String = id + "/" + span.kind.toString + override def toString: String = id.toString + "/" + span.kind.toString /* classification */