diff options
Diffstat (limited to 'tools/Makefile.cmt2ml')
| -rw-r--r-- | tools/Makefile.cmt2ml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/tools/Makefile.cmt2ml b/tools/Makefile.cmt2ml new file mode 100644 index 0000000000..b034e7b9cd --- /dev/null +++ b/tools/Makefile.cmt2ml @@ -0,0 +1,12 @@ +TARGET=cmt2ml +MLIS= +MLS=cmt2ml.ml +CMAS= unix.cma toplevellib.cma +INCLUDES= \ + -I ../ocaml-binary-annot/typing \ + -I ../ocaml-binary-annot/parsing \ + -I ../ocaml-binary-annot/utils \ + +OFLAGS=-g -annot + +include Makefile.rules |