From 2ce14b28c905c6fdfb6084fd30137c6f4e4e0701 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Wed, 5 Jul 2023 15:59:40 +0200
Subject: [PATCH] Remove duplicate feature.xml requires entries
---
org.eventb.texteditor.feature/feature.xml | 3 ---
1 file changed, 3 deletions(-)
diff --git a/org.eventb.texteditor.feature/feature.xml b/org.eventb.texteditor.feature/feature.xml
index 48831d7..83a6dd8 100644
--- a/org.eventb.texteditor.feature/feature.xml
+++ b/org.eventb.texteditor.feature/feature.xml
@@ -182,12 +182,10 @@ Inc. in the United States, other countries, or both.
<import plugin="org.eclipse.ui.editors" version="3.8.0" match="compatible"/>
<import plugin="org.eclipse.ui.ide" version="3.8.2" match="compatible"/>
<import plugin="org.eclipse.ui.workbench.texteditor"/>
- <import plugin="org.eclipse.core.resources" version="3.8.1" match="greaterOrEqual"/>
<import plugin="org.eventb.emf.core" version="4.0.0"/>
<import plugin="org.eclipse.core.runtime" version="3.10.0" match="greaterOrEqual"/>
<import plugin="org.eclipse.emf.ecore.xmi" version="2.10.1" match="greaterOrEqual"/>
<import plugin="org.rodinp.core" version="1.7.0" match="greaterOrEqual"/>
- <import plugin="org.eventb.core" version="3.1.0" match="greaterOrEqual"/>
<import plugin="org.eclipse.emf.edit"/>
<import plugin="org.eventb.texteditor.parsers"/>
<import plugin="org.rodinp.keyboard.core" version="2.0.0" match="compatible"/>
@@ -198,7 +196,6 @@ Inc. in the United States, other countries, or both.
<import plugin="org.eclipse.emf.compare.edit" version="4.0.0" match="greaterOrEqual"/>
<import plugin="org.eclipse.emf.compare.ide" version="3.1.1" match="greaterOrEqual"/>
<import plugin="org.eclipse.emf.compare.rcp" version="2.2.0" match="greaterOrEqual"/>
- <import plugin="org.eventb.core" version="3.1.0" match="compatible"/>
</requires>
<plugin
--
GitLab