author | wenzelm |
Tue, 29 Sep 2015 16:45:54 +0200 | |
changeset 61279 | 8410015c3e82 |
parent 61278 | 4d2ea32e0f75 |
child 61280 | 12f9ab87a06d |
--- a/src/Pure/GUI/system_dialog.scala Tue Sep 29 16:28:02 2015 +0200 +++ b/src/Pure/GUI/system_dialog.scala Tue Sep 29 16:45:54 2015 +0200 @@ -111,7 +111,7 @@ setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE) addWindowListener(new WindowAdapter { - override def windowClosed(e: WindowEvent) { + override def windowClosing(e: WindowEvent) { if (_return_code.isDefined) conclude() else stopping() }