From 764c92f056e1a8b801ac952cc545444f50ef0cdd Mon Sep 17 00:00:00 2001 From: Philipp Gesang Date: Fri, 16 May 2014 20:36:30 +0200 Subject: add gitignore --- .gitignore | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 .gitignore 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 + + -- cgit v1.2.3