author | wenzelm |
Wed, 30 Sep 2015 20:48:59 +0200 | |
changeset 61292 | ca76026ed7cc |
parent 61291 | e00e1bf23d03 |
child 61293 | 876e7eae22be |
--- a/src/Tools/jEdit/src/session_build.scala Wed Sep 30 20:02:39 2015 +0200 +++ b/src/Tools/jEdit/src/session_build.scala Wed Sep 30 20:48:59 2015 +0200 @@ -103,7 +103,7 @@ if (can_auto_close) conclude() else { val button = - new Button(if (_return_code == Some(0)) "OK" else "Exit") { + new Button(if (_return_code == Some(0)) "OK" else "Close") { reactions += { case ButtonClicked(_) => conclude() } } set_actions(button)