changeset 67858 | cba5c5657378 |
parent 65920 | 9e65c03e94da |
child 71785 | 39613d6e2021 |
--- a/src/Pure/General/timing.scala Wed Mar 14 16:52:16 2018 +0100 +++ b/src/Pure/General/timing.scala Wed Mar 14 17:43:30 2018 +0100 @@ -70,4 +70,7 @@ } override def toString: String = message + + def json: JSON.Object.T = + JSON.Object("elapsed" -> elapsed.seconds, "cpu" -> cpu.seconds, "gc" -> gc.seconds) }