# HG changeset patch # User wenzelm # Date 1730728221 -3600 # Node ID e181259e539b99c6bca1d4fa1be436a64333e3ab # Parent 545d474ada44271ca9e12ff18b3c431a7e61a2e1 more accurate Symbol.Metric, following 6eccae338770; diff -r 545d474ada44 -r e181259e539b src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Mon Nov 04 14:39:27 2024 +0100 +++ b/src/Pure/General/symbol.scala Mon Nov 04 14:50:21 2024 +0100 @@ -673,7 +673,9 @@ def apply(str: String): Double = (for (s <- iterator(str)) yield { val sym = encode(s) - if (sym.startsWith("\\