--- 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)
}