Browse Source

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
master
Dave Parker 15 years ago
parent
commit
65c2f23e71
  1. 7
      prism/src/userinterface/GUIPrism.java

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

Loading…
Cancel
Save