diff -r 49b964a6fe11 -r 0f8187611ba9 src/Tools/jEdit/src/session_build.scala --- a/src/Tools/jEdit/src/session_build.scala Wed Sep 30 23:37:20 2015 +0200 +++ b/src/Tools/jEdit/src/session_build.scala Wed Sep 30 23:54:22 2015 +0200 @@ -102,10 +102,7 @@ { if (can_auto_close) conclude() else { - val button = - new Button(if (_return_code == Some(0)) "OK" else "Close") { - reactions += { case ButtonClicked(_) => conclude() } - } + val button = new Button("Close") { reactions += { case ButtonClicked(_) => conclude() } } set_actions(button) button.peer.getRootPane.setDefaultButton(button.peer) }