From 116cd985471189926c6abfa7d6c4f62c95977dc1 Mon Sep 17 00:00:00 2001 From: dgelessus <dgelessus@users.noreply.github.com> Date: Mon, 20 Jan 2020 11:55:42 +0100 Subject: [PATCH] Re-add some .gitignore entries that were needed after all --- .gitignore | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.gitignore b/.gitignore index 61f75f4..da7d8d8 100644 --- a/.gitignore +++ b/.gitignore @@ -6,3 +6,8 @@ .classpath .project .settings/ + +# Test output +*.prob +Testing.cfg +Testing.tla -- GitLab