# 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)