aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-01-30 22:19:16 +0100
committerGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-02-24 14:07:06 +0100
commit5aded353dbf4eccff16769e3762c4810060fb6cf (patch)
tree44e77c4c419946c8e0596d86d6aaa92f57dcfd47 /.gitignore
parentb0b9a582d99d57d9f9c6f4b322911102cca734ff (diff)
Fix coqide build under MacOS
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore1
1 files changed, 0 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore
index 8f0a9a409..5b4ffa77b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -139,7 +139,6 @@ tactics/extratactics.ml
tactics/extraargs.ml
toplevel/whelp.ml
ide/coqide_main.ml
-ide/coqide_main_opt.ml
# other auto-generated files