# HG changeset patch
# User wenzelm
# Date 1730750431 -3600
# Node ID 2b9ffffccc9be9d9a89ea3a700e34c69e52dd28e
# Parent  30f7eb65d679c3b13a8a397bd0d868773ea813d1
tuned;

diff -r 30f7eb65d679 -r 2b9ffffccc9b src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Mon Nov 04 20:55:01 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Mon Nov 04 21:00:31 2024 +0100
@@ -1560,7 +1560,7 @@
     val line_height = Font_Metric.default.height
     val char_width = Font_Metric.default.average_width
     val padding = Font_Metric.default.space_width
-    val gap = Font_Metric.default.average_width * 3
+    val gap = char_width * 3
 
     val graph = schedule.graph