From fbcbf7975cd2464638b9ca6055a5a22494e48946 Mon Sep 17 00:00:00 2001
From: Luca Frosini <luca.frosini@isti.cnr.it>
Date: Thu, 8 Oct 2020 15:18:50 +0200
Subject: [PATCH] Ignored eclipse project files

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

diff --git a/.settings/.gitignore b/.settings/.gitignore
new file mode 100644
index 0000000..3b1537c
--- /dev/null
+++ b/.settings/.gitignore
@@ -0,0 +1 @@
+/org.eclipse.jdt.core.prefs
diff --git a/.settings/org.eclipse.jdt.core.prefs b/.settings/org.eclipse.jdt.core.prefs
deleted file mode 100644
index 714351a..0000000
--- a/.settings/org.eclipse.jdt.core.prefs
+++ /dev/null
@@ -1,5 +0,0 @@
-eclipse.preferences.version=1
-org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8
-org.eclipse.jdt.core.compiler.compliance=1.8
-org.eclipse.jdt.core.compiler.problem.forbiddenReference=warning
-org.eclipse.jdt.core.compiler.source=1.8