From 4c4e341807117a4f61df5d338c138b37461ca9c1 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Wed, 5 Jul 2023 16:55:18 +0200
Subject: [PATCH] Remove duplicate category.xml under
 org.eventb.texteditor.feature

---
 org.eventb.texteditor.feature/category.xml | 7 -------
 1 file changed, 7 deletions(-)
 delete mode 100644 org.eventb.texteditor.feature/category.xml

diff --git a/org.eventb.texteditor.feature/category.xml b/org.eventb.texteditor.feature/category.xml
deleted file mode 100644
index 32e3567..0000000
--- a/org.eventb.texteditor.feature/category.xml
+++ /dev/null
@@ -1,7 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<site>
-   <feature url="features/org.eventb.texteditor.feature_3.4.1.qualifier.jar" id="org.eventb.texteditor.feature" version="3.4.1.qualifier">
-      <category name="camille"/>
-   </feature>
-   <category-def name="camille" label="camille"/>
-</site>
-- 
GitLab