From b067b0820d6c923974a2baa37c9a15277bd247f1 Mon Sep 17 00:00:00 2001 From: dgelessus <dgelessus@users.noreply.github.com> Date: Thu, 6 Jul 2023 14:49:12 +0200 Subject: [PATCH] Remove stray .gitignore --- org.eventb.texteditor.parsers/.gitignore | 1 - 1 file changed, 1 deletion(-) delete mode 100644 org.eventb.texteditor.parsers/.gitignore diff --git a/org.eventb.texteditor.parsers/.gitignore b/org.eventb.texteditor.parsers/.gitignore deleted file mode 100644 index ae3c172..0000000 --- a/org.eventb.texteditor.parsers/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/bin/ -- GitLab