summaryrefslogtreecommitdiffstats
path: root/utils/clflags.mli
diff options
context:
space:
mode:
Diffstat (limited to 'utils/clflags.mli')
-rw-r--r--utils/clflags.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/utils/clflags.mli b/utils/clflags.mli
index 038c3aacb..876776acd 100644
--- a/utils/clflags.mli
+++ b/utils/clflags.mli
@@ -55,6 +55,7 @@ val dllpaths : string list ref
val make_package : bool ref
val for_package : string option ref
val error_size : int ref
+val transparent_modules : bool ref
val dump_source : bool ref
val dump_parsetree : bool ref
val dump_typedtree : bool ref