From fb8e41ba16f3d52faabff5737ecdd80eb4715e82 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Tue, 14 Jun 2016 11:10:10 +0200
Subject: configure: use ln on linux and cp on windows

---
 .gitignore | 4 ++++
 1 file changed, 4 insertions(+)

(limited to '.gitignore')

diff --git a/.gitignore b/.gitignore
index 0193c9dfa..56e190598 100644
--- a/.gitignore
+++ b/.gitignore
@@ -138,6 +138,10 @@ tools/tolink.ml
 theories/Numbers/Natural/BigN/NMake_gen.v
 ide/index_urls.txt
 lia.cache
+checker/names.ml
+checker/names.mli
+checker/esubst.ml
+checker/esubst.mli
 
 # mlis documentation
 
-- 
cgit v1.2.3