diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..96e9cbd --- /dev/null +++ b/.gitignore @@ -0,0 +1,5 @@ +*.cmi +*.cmx +*.o +*.a +/tipe diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..b26e1a7 --- /dev/null +++ b/Makefile @@ -0,0 +1,7 @@ + + +%.cmx: %.ml + ocamlopt -c $< + +tipe: tipe.cmx + ocamlopt -o tipe str.cmxa tipe.cmx