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