Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper GUI.copy_font, following fd3b214b0979;
authorwenzelm
Thu, 21 Aug 2025 20:09:16 +0200
changeset 83024 0b7cc1bf68e8
parent 83023 56d2510fd5ac
child 83025 0a07631c6e17
proper GUI.copy_font, following fd3b214b0979;
src/Tools/jEdit/src/status_widget.scala file | annotate | diff | comparison | revisions 
--- a/src/Tools/jEdit/src/status_widget.scala	Thu Aug 21 20:07:40 2025 +0200
+++ b/src/Tools/jEdit/src/status_widget.scala	Thu Aug 21 20:09:16 2025 +0200
@@ -25,7 +25,7 @@
   abstract class GUI(view: View) extends JComponent {
     /* init */
 
-    setFont(GUI.label_font())
+    setFont(GUI.copy_font(GUI.label_font()))
 
     private val font_render_context = new FontRenderContext(null, true, false)
     private val line_metrics = getFont.getLineMetrics(template, font_render_context)
isabelle