diff options
-rw-r--r-- | .gitignore | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..5ccc4e9 --- /dev/null +++ b/.gitignore @@ -0,0 +1,25 @@ +# from https://github.com/github/gitignore/blob/master/OCaml.gitignore +*.annot +*.cmo +*.cma +*.cmi +*.a +*.o +*.cmx +*.cmxs +*.cmxa + +# omake +.omakedb +.omakedb.lock +*.omc + +# other stuff in the tree +context_mirror_bot_id_rsa +context_mirror_bot_id_rsa.pub +context_mirror_bot +*.run +*.html +*.log + + |