From f377960d80f5a31620b1105758b0c24aef828cd3 Mon Sep 17 00:00:00 2001
From: Matej Košík <matej.kosik@inria.fr>
Date: Mon, 12 Jun 2017 19:28:52 +0200
Subject: Store plugins/micromega/micromega.{ml,mli} files in the repository.
 Try to generate them later.

---
 .gitignore | 4 ----
 1 file changed, 4 deletions(-)

(limited to '.gitignore')

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
-- 
cgit v1.2.3