diff --git a/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java b/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java index 4bbe282bcfb7ed929ee4e66951746ad85f7954c2..28cfabb12da42127692e7bbbf8efb864db3c90f0 100644 --- a/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java +++ b/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java @@ -206,8 +206,8 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements + rootElement.getClass()); } - // shutdown animator - animator.shutdown(); + // TODO: should i shutdown the animator? + // animator.shutdown(); } catch (ProBException e) { e.notifyUserOnce(); throw new ExecutionException("Unit Analysis Failed", e);