diff options
author | Philipp Gesang <phg42.2a@gmail.com> | 2014-05-16 20:36:30 +0200 |
---|---|---|
committer | Philipp Gesang <phg42.2a@gmail.com> | 2014-05-16 20:36:30 +0200 |
commit | 764c92f056e1a8b801ac952cc545444f50ef0cdd (patch) | |
tree | bdc6c75d5f054737acc689ea2c40472fca528e33 | |
parent | 94aa3d0f8c4c480ad67045f12d33b0f7813868e6 (diff) | |
download | context-mirror-bot-764c92f056e1a8b801ac952cc545444f50ef0cdd.tar.gz |
add gitignore
-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 + + |