From e16940af94bb4e03db6a0e2e21311666380f0bf0 Mon Sep 17 00:00:00 2001
From: Luca Frosini <luca.frosini@isti.cnr.it>
Date: Thu, 7 Apr 2022 11:44:04 +0200
Subject: [PATCH] Removed IDE specific file

---
 .settings/.gitignore                       | 1 +
 .settings/org.eclipse.core.resources.prefs | 5 -----
 2 files changed, 1 insertion(+), 5 deletions(-)
 delete mode 100644 .settings/org.eclipse.core.resources.prefs

diff --git a/.settings/.gitignore b/.settings/.gitignore
index 3b1537c..57d3934 100644
--- a/.settings/.gitignore
+++ b/.settings/.gitignore
@@ -1 +1,2 @@
 /org.eclipse.jdt.core.prefs
+/org.eclipse.core.resources.prefs
diff --git a/.settings/org.eclipse.core.resources.prefs b/.settings/org.eclipse.core.resources.prefs
deleted file mode 100644
index cdfe4f1..0000000
--- a/.settings/org.eclipse.core.resources.prefs
+++ /dev/null
@@ -1,5 +0,0 @@
-eclipse.preferences.version=1
-encoding//src/main/java=UTF-8
-encoding//src/test/java=UTF-8
-encoding//src/test/resources=UTF-8
-encoding/<project>=UTF-8