diff --git a/org.eventb.texteditor.parsers/.gitignore b/org.eventb.texteditor.parsers/.gitignore deleted file mode 100644 index ae3c1726048cd06b9a143e0376ed46dd9b9a8d53..0000000000000000000000000000000000000000 --- a/org.eventb.texteditor.parsers/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/bin/