# HG changeset patch
# User wenzelm
# Date 1730715664 -3600
# Node ID cb31fd7c4bce093391d641e5f2a6857dd4abeb3c
# Parent  f94b30fa2b6c96eba92d7c34f391d7629140452f
tuned GUI (again, see 0521e65af41e);

diff -r f94b30fa2b6c -r cb31fd7c4bce src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Sun Nov 03 22:29:07 2024 +0100
+++ b/src/Pure/GUI/gui.scala	Mon Nov 04 11:21:04 2024 +0100
@@ -51,7 +51,6 @@
 
     // see https://www.formdev.com/flatlaf/customizing
     UIManager.put("Component.arrowType", "triangle")
-    UIManager.put("ScrollBar.showButtons", true)
   }