diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-13 01:05:14 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-13 01:05:14 +0200 |
| commit | 598ec175ea8ba6b424cc9ecf87f878494aef69a8 (patch) | |
| tree | d536c451975fcecc3ca6c704c075c2f03d03a9cc /.gitignore | |
| parent | 7e9a4aa4efa62d9fcded340c1c2f07a73021aca0 (diff) | |
| parent | f377960d80f5a31620b1105758b0c24aef828cd3 (diff) | |
Merge PR#772: 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 |