From 65c2f23e71874dd00bd05207d1004686b72b063b Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 3 Dec 2010 11:19:26 +0000 Subject: [PATCH] GUI does not bug user to save settings on exit. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2318 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/userinterface/GUIPrism.java | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/prism/src/userinterface/GUIPrism.java b/prism/src/userinterface/GUIPrism.java index 798edd62..dd13031d 100644 --- a/prism/src/userinterface/GUIPrism.java +++ b/prism/src/userinterface/GUIPrism.java @@ -407,8 +407,8 @@ public class GUIPrism extends JFrame doExit = true; notifyEventListeners(new GUIExitEvent(GUIExitEvent.REQUEST_EXIT)); - if(prism.getSettings().isModified()) - { + // Don't bug user to save defaults on exit + /*if (prism.getSettings().isModified()) { String[] selection = {"Yes", "No", "Cancel"}; @@ -432,8 +432,7 @@ public class GUIPrism extends JFrame case 2: doExit = false; default: doExit = false; } - - } + }*/ if (doExit) System.exit(0); }