From 76d310da8b1ad9deee3479799c130644316e65aa Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Fri, 15 Aug 2014 20:51:31 -0700 Subject: [PATCH] chore(library/.gitignore): add TAGS --- library/.gitignore | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/library/.gitignore b/library/.gitignore index 546197d23..d9a3e979b 100644 --- a/library/.gitignore +++ b/library/.gitignore @@ -1 +1,2 @@ -.lean_options \ No newline at end of file +.lean_options +TAGS \ No newline at end of file