author | wenzelm |
Wed, 22 Apr 2020 18:37:25 +0200 | |
changeset 71785 | 39613d6e2021 |
parent 71784 | 8a5da740e388 |
child 71786 | 97975476547c |
--- 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)