From f17ce9cfe98e083eb18ed3da56e8ad7b4ffef53a Mon Sep 17 00:00:00 2001
From: Jens Bendisposto <jens@bendisposto.de>
Date: Tue, 13 Nov 2012 10:57:10 +0100
Subject: [PATCH] Replaced new export handler by the old version
---
de.prob.ui/plugin.xml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/de.prob.ui/plugin.xml b/de.prob.ui/plugin.xml
index 31a3a0a8..a8edde20 100644
--- a/de.prob.ui/plugin.xml
+++ b/de.prob.ui/plugin.xml
@@ -727,7 +727,7 @@
<handler
commandId="de.prob.ui.newcore.export">
<class
- class="de.prob.ui.eventb.ExportNewCoreHandler">
+ class="de.prob.ui.eventb.ExportClassicHandler">
</class>
<enabledWhen>
<with
--
GitLab