From 73cd48cb130185f6a8802f747719ae05a534e455 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 27 Dec 2013 16:46:17 -0800 Subject: [PATCH] chore(.gitignore): ignore .md.lean files Signed-off-by: Leonardo de Moura --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 06c6dcc1b..28688dde8 100644 --- a/.gitignore +++ b/.gitignore @@ -2,6 +2,7 @@ .lean_trace *.produced.out *.md.lua +*.md.lean a.out build GPATH