summaryrefslogtreecommitdiff
path: root/tools/ocamlcp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/ocamlcp.ml')
-rw-r--r--tools/ocamlcp.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/ocamlcp.ml b/tools/ocamlcp.ml
index 278952f75e..0aeaf2ce1b 100644
--- a/tools/ocamlcp.ml
+++ b/tools/ocamlcp.ml
@@ -126,6 +126,7 @@ module Options = Main_args.Make_bytecomp_options (struct
let _dflambda = option "-dflambda"
let _dinstr = option "-dinstr"
let _dtimings = option "-dtimings"
+ let _dprofile = option "-dprofile"
let _args = Arg.read_arg
let _args0 = Arg.read_arg0
let anonymous = process_file