aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cbytegen.mli
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-30 09:25:44 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-30 09:25:44 +0200
commit8c3d9eb165b456fc83753624efe6708832e9b52f (patch)
treef0c7050b1b2fcaa63167e8830c535d1dde982f35 /kernel/cbytegen.mli
parent14226761af6525c9848f3626cd86b0d4e47dad4d (diff)
parentce9b17821a3be3dee7fa7e49c35edaefc658b965 (diff)
Merge PR #6958: [lib] Move global options to their proper place.
Diffstat (limited to 'kernel/cbytegen.mli')
-rw-r--r--kernel/cbytegen.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index abab58b60..1c4cdcbeb 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -25,3 +25,6 @@ val compile_constant_body : fail_on_error:bool ->
(** Shortcut of the previous function used during module strengthening *)
val compile_alias : Names.Constant.t -> body_code
+
+(** Dump the bytecode after compilation (for debugging purposes) *)
+val dump_bytecode : bool ref