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