src/Pure/General/pretty.scala

--- a/src/Pure/General/pretty.scala	Mon Nov 04 14:50:21 2024 +0100
+++ b/src/Pure/General/pretty.scala	Mon Nov 04 20:55:01 2024 +0100
@@ -49,7 +49,7 @@
   /* text metric -- standardized to width of space */
 
   abstract class Metric {
-    val unit: Double
+    def unit: Double
     def apply(s: String): Double
   }