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