From 5e5817678b8678997a479f5585ed5e6373da8559 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 9 Nov 2018 16:00:28 +0100
Subject: Add .cmt and generated ml files to gitignore

---
 .gitignore           | 5 ++++-
 tuto2/src/.gitignore | 1 +
 2 files changed, 5 insertions(+), 1 deletion(-)
 create mode 100644 tuto2/src/.gitignore

diff --git a/.gitignore b/.gitignore
index 6efd03647c..3e4978fac4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,5 @@
 *.ml*.d
-*.cm[ix]*
+*.cm[ixt]*
 Makefile.coq*
 *~
 *.[ao]
@@ -8,3 +8,6 @@ Makefile.coq*
 *.glob
 *.aux
 */*/.merlin
+
+# by convention g_foo.ml is generated
+g_*.ml
diff --git a/tuto2/src/.gitignore b/tuto2/src/.gitignore
new file mode 100644
index 0000000000..5b1b6a902e
--- /dev/null
+++ b/tuto2/src/.gitignore
@@ -0,0 +1 @@
+/demo.ml
-- 
cgit v1.2.3