changeset 11931 | a5d1c9b34900 |
parent 11875 | 5fcf6b6436af |
child 14981 | e73f8140af78 |
--- a/lib/browser/GraphBrowser/GraphBrowserFrame.java Thu Oct 25 02:13:02 2001 +0200 +++ b/lib/browser/GraphBrowser/GraphBrowserFrame.java Thu Oct 25 16:09:39 2001 +0200 @@ -117,5 +117,10 @@ mb.add(m1); setMenuBar(mb); add("Center", br); + addWindowListener( new WindowAdapter() { + public void windowClosing(WindowEvent e) { + System.exit(0); + } + }); } }