# HG changeset patch # User wenzelm # Date 1587573445 -7200 # Node ID 39613d6e20218b35038c2c05da737f4626035bab # Parent 8a5da740e388ff7a6dd68e3dd6d8a65d1308ee36 avoid deprecated operations; diff -r 8a5da740e388 -r 39613d6e2021 src/Pure/General/timing.scala --- a/src/Pure/General/timing.scala Wed Apr 22 18:37:09 2020 +0200 +++ b/src/Pure/General/timing.scala Wed Apr 22 18:37:25 2020 +0200 @@ -60,7 +60,7 @@ { val factor_text = factor match { - case Some(f) => String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(f)) + case Some(f) => String.format(Locale.ROOT, ", factor %.2f", java.lang.Double.valueOf(f)) case None => "" } if (resources.seconds >= 3.0)