Improved the .gitignore file.

collaborativetrust · Aug 15, 2009 · 91ae849 · 91ae849
1 parent 246faec
commit 91ae849
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/.gitignore b/.gitignore
@@ -16,6 +16,11 @@ pickwiki
 *.cmi
 *.cmx
 *.o
+*.annot
+*.a
+*.cma
+*.cmxa
+filesystem_store
 .depends
 eval_online_wiki
 vote_revision