# HG changeset patch
# User wenzelm
# Date 1614870510 -3600
# Node ID 5e312d6bb883e3b80794d0bd12d662127f296001
# Parent  dde25151c3c170e90308ab43867054c5cff62bd5
tuned --- fewer warnings;

diff -r dde25151c3c1 -r 5e312d6bb883 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 */