lib/browser/GraphBrowser/GraphBrowserFrame.java
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);
+      }
+    });
 	}
 }