diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000000000000000000000000000000000000..cf100fb9a27349a5d8a01f064419d146c7870f48 --- /dev/null +++ b/.gitignore @@ -0,0 +1,12 @@ +# files created by editors +.*.swp +*~ +# make subsidiary files +.depend +# c++-object files +*.o +*.a +# caml-files +*.cmxa +*.cmi +*.cmx