src/Pure/GUI/wrap_panel.scala
changeset 78243 0e221a8128e4
parent 75393 87ebf5a50283
--- a/src/Pure/GUI/wrap_panel.scala	Sun Jul 02 18:56:52 2023 +0200
+++ b/src/Pure/GUI/wrap_panel.scala	Sun Jul 02 19:05:59 2023 +0200
@@ -33,7 +33,7 @@
     private def layout_size(target: Container, preferred: Boolean): Dimension = {
       target.getTreeLock.synchronized {
         val target_width =
-          if (target.getSize.width == 0) Integer.MAX_VALUE
+          if (target.getSize.width == 0) Int.MaxValue
           else target.getSize.width
 
         val hgap = getHgap