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

---
 tuto2/src/.gitignore | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 tuto2/src/.gitignore

(limited to 'tuto2')

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