From d24258a17f08ecded8093cc49327af96fba84893 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Fri, 4 Jan 2013 12:46:11 +0100
Subject: [PATCH] update log message for unit analysis
---
.../src/de/prob/ui/eventb/StartUnitAnalysisHandler.java | 6 +-----
1 file changed, 1 insertion(+), 5 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 f404a08b..919f0979 100644
--- a/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java
+++ b/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java
@@ -116,14 +116,10 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
;
if (resource != null) {
- LimitedLogger.getLogger().log("user started animation",
+ LimitedLogger.getLogger().log("user started unit analysis",
rootElement.getElementName(), null);
registerModificationListener(resource);
- // do not change perspective - just start animator and shut it down
- // after the analysis
- // PerspectiveFactory.openPerspective();
-
final Animator animator = Animator.getAnimator();
try {
// load machine and activate plugin
--
GitLab