diff options
| author | Théo Zimmermann | 2018-10-20 13:27:40 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-10-20 13:27:40 +0200 |
| commit | 16e0223e111cdf1c61c421617dfda08de6e96720 (patch) | |
| tree | c7c9dc5e9f1f519caa4fb2a0a6f46e1ec68e4608 | |
| parent | 02f7b4ac1968ca4522d144e34b52dead3871a8b7 (diff) | |
| parent | d48f7c7bd8d297c61de2dcb3b4e44c340de8edaf (diff) | |
Merge PR #8782: gitignore test-suite/.nia.cache
| -rw-r--r-- | .gitignore | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/.gitignore b/.gitignore index f741135211..538124b8e5 100644 --- a/.gitignore +++ b/.gitignore @@ -68,6 +68,7 @@ time-of-build-after.log .csdp.cache test-suite/.lia.cache test-suite/.nra.cache +test-suite/.nia.cache test-suite/trace test-suite/misc/universes/all_stdlib.v test-suite/misc/universes/universes.txt @@ -165,8 +166,6 @@ checker/esubst.mli user-contrib .*.sw* .#* -test-suite/.lia.cache -test-suite/.nra.cache plugins/ssr/ssrparser.ml plugins/ssr/ssrvernac.ml |