summaryrefslogtreecommitdiff
path: root/driver/optmain.ml
diff options
context:
space:
mode:
Diffstat (limited to 'driver/optmain.ml')
-rw-r--r--driver/optmain.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/driver/optmain.ml b/driver/optmain.ml
index c069cb4f8e..f28be9aec4 100644
--- a/driver/optmain.ml
+++ b/driver/optmain.ml
@@ -105,6 +105,8 @@ module Options = Main_args.Make_optcomp_options (struct
let _a = set make_archive
let _absname = set Location.absname
+ let _afl_instrument = set afl_instrument
+ let _afl_inst_ratio n = afl_inst_ratio := n
let _annot = set annotations
let _binannot = set binary_annotations
let _c = set compile_only