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