From 226f3010445bde2a6713aef37f855e9fb1c55149 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Fri, 29 Aug 2014 01:35:19 -0700 Subject: [PATCH] chore(library/.gitignore): update --- library/.gitignore | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/library/.gitignore b/library/.gitignore index d9a3e979b..1e9d24c88 100644 --- a/library/.gitignore +++ b/library/.gitignore @@ -1,2 +1,4 @@ -.lean_options -TAGS \ No newline at end of file +TAGS +build.ninja +.ninja_deps +.ninja_log