changeset 61292 | ca76026ed7cc |
parent 61289 | 14cd4eabce10 |
child 61299 | 0f8187611ba9 |
--- 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)