diff options
| author |  Matej Košík <matej.kosik@inria.fr> | 2017-06-12 19:28:52 +0200 |
|---|---|---|
| committer | Matej Košík <matej.kosik@inria.fr> | 2017-06-12 19:33:22 +0200 |
| commit | f377960d80f5a31620b1105758b0c24aef828cd3 (patch) | |
| tree | 2bb842c6645e62686f110e02912e8bcded6b5d2f /.gitignore | |
| parent | 83d8b081c02cfde83c8fd93102f8f1aae3fe87b3 (diff) | |
Store plugins/micromega/micromega.{ml,mli} files in the repository. Try to generate them later.
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/.gitignore b/.gitignore index fa83045e7..f66e8dcd8 100644 --- a/.gitignore +++ b/.gitignore @@ -179,9 +179,5 @@ user-contrib test-suite/.lia.cache test-suite/.nra.cache -# these files are generated from plugins/micromega/MExtraction.v -plugins/micromega/micromega.ml -plugins/micromega/micromega.mli - plugins/ssr/ssrparser.ml plugins/ssr/ssrvernac.ml |