chore(library): add .gitignore
[skip ci]
This commit is contained in:
parent
74dafe76bb
commit
87632622ee
1 changed files with 1 additions and 0 deletions
1
library/.gitignore
vendored
Normal file
1
library/.gitignore
vendored
Normal file
|
@ -0,0 +1 @@
|
|||
.lean_options
|
Loading…
Reference in a new issue