diff options
Diffstat (limited to 'tools/Makefile.cmt2annot')
| -rw-r--r-- | tools/Makefile.cmt2annot | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/tools/Makefile.cmt2annot b/tools/Makefile.cmt2annot new file mode 100644 index 0000000000..6327348cc9 --- /dev/null +++ b/tools/Makefile.cmt2annot @@ -0,0 +1,12 @@ +TARGET=cmt2annot +MLIS= +MLS=cmt2annot.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 |