From aa4363a0607a27a21efd90432ed9503262ef682f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Nov 2013 14:14:23 -0800 Subject: [PATCH] chore(.gitignore): hide '*.md.lua' files Signed-off-by: Leonardo de Moura --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 57ff7f85b7..3444fdbe73 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,7 @@ *~ .lean_trace *.produced.out +*.md.lua a.out build GPATH