diff --git a/.gitignore b/.gitignore new file mode 100644 index 00000000..999cfd3f --- /dev/null +++ b/.gitignore @@ -0,0 +1,14 @@ +*.cmi +*.cmo +*.cmx +*.cmxs +*.o +*.a +*.annot +META +basic.mli +out.html +read.ml +ydump +yojson.ml +yojson.mli