add gitignore

ChrisHughes24 · May 6, 2023 · 2cf1419 · 2cf1419
1 parent 119b68f
commit 2cf1419
Showing 1 changed file with 12 additions and 0 deletions.
diff --git a/.gitignore b/.gitignore
@@ -0,0 +1,12 @@
+*.olean
+/_target
+/leanpkg.path
+_cache
+__pycache__
+all.lean
+*.depend
+/src/.noisy_files
+*~
+.DS_Store
+*.lock
+port_status.yaml