From 9a22c88518b58c08e791390985fb3744c64baeb5 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Thu, 3 Jan 2013 15:30:21 +0100
Subject: [PATCH] do not should down the animator after unit analysis. not sure
if this is correct anyway.
---
.../src/de/prob/ui/eventb/StartUnitAnalysisHandler.java | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
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 4bbe282b..28cfabb1 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);
--
GitLab