From fcb6c715176e773e8e68c6c752e92442eaa63e60 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Fri, 29 Aug 2014 02:51:22 -0700 Subject: [PATCH] chore(library): add .project file --- library/.project | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 library/.project diff --git a/library/.project b/library/.project new file mode 100644 index 000000000..9330a2051 --- /dev/null +++ b/library/.project @@ -0,0 +1,3 @@ ++ *.lean +- flycheck*.lean +- .#*.lean \ No newline at end of file