src/Tools/jEdit/src/session_build.scala
changeset 61292 ca76026ed7cc
parent 61289 14cd4eabce10
child 61299 0f8187611ba9
equal deleted inserted replaced
61291:e00e1bf23d03 61292:ca76026ed7cc
   101       GUI_Thread.delay_first(Time.seconds(1.0))
   101       GUI_Thread.delay_first(Time.seconds(1.0))
   102       {
   102       {
   103         if (can_auto_close) conclude()
   103         if (can_auto_close) conclude()
   104         else {
   104         else {
   105           val button =
   105           val button =
   106             new Button(if (_return_code == Some(0)) "OK" else "Exit") {
   106             new Button(if (_return_code == Some(0)) "OK" else "Close") {
   107               reactions += { case ButtonClicked(_) => conclude() }
   107               reactions += { case ButtonClicked(_) => conclude() }
   108             }
   108             }
   109           set_actions(button)
   109           set_actions(button)
   110           button.peer.getRootPane.setDefaultButton(button.peer)
   110           button.peer.getRootPane.setDefaultButton(button.peer)
   111         }
   111         }