# HG changeset patch # User wenzelm # Date 1607616546 -3600 # Node ID 0ad513706a27a59f19ae9d0e2807d301a7771887 # Parent 530534f2f0fd9428ae4be522b20e00a7c9923402 clarified Pretty.Metric, as for build errors; diff -r 530534f2f0fd -r 0ad513706a27 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Thu Dec 10 17:01:59 2020 +0100 +++ b/src/Pure/Tools/build_job.scala Thu Dec 10 17:09:06 2020 +0100 @@ -88,7 +88,7 @@ progress: Progress = new Progress, margin: Double = Pretty.default_margin, breakgain: Double = Pretty.default_breakgain, - metric: Pretty.Metric = Pretty.Default_Metric, + metric: Pretty.Metric = Symbol.Metric, unicode_symbols: Boolean = false) { val store = Sessions.store(options)