aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Matej Kosik <matej.kosik@inria.fr>2016-10-19 16:42:03 +0200
committerGravatar Matej Kosik <matej.kosik@inria.fr>2016-10-19 16:42:03 +0200
commit102e62afb98903c7c6be667aa9641dc7be4ca34d (patch)
tree6baaca85f6098ee03858e266bf365ea095934c2f
parentb403e0224ba502c0cd80702eca08405aa6de0828 (diff)
enriching ".gitignore"
-rw-r--r--.gitignore2
1 files changed, 2 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index 9653564d4..4cce21c82 100644
--- a/.gitignore
+++ b/.gitignore
@@ -161,3 +161,5 @@ dev/myinclude
user-contrib
.*.sw*
+test-suite/.lia.cache
+test-suite/.nra.cache