tuned --- fewer warnings;
authorwenzelm
Thu, 04 Mar 2021 16:08:30 +0100
changeset 73610 5e312d6bb883
parent 73609 dde25151c3c1
child 73611 6bf6160a2c54
tuned --- fewer warnings;
src/Pure/PIDE/command.scala
--- 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 */