diff options
Diffstat (limited to 'utils/clflags.mli')
| -rw-r--r-- | utils/clflags.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/utils/clflags.mli b/utils/clflags.mli index 4cff375a4..4ec62cc8d 100644 --- a/utils/clflags.mli +++ b/utils/clflags.mli @@ -31,6 +31,7 @@ val classic : bool ref val nopervasives : bool ref val preprocessor : string option ref val annotations : bool ref +val binary_annotations : bool ref val use_threads : bool ref val use_vmthreads : bool ref val noassert : bool ref @@ -80,3 +81,4 @@ val std_include_dir : unit -> string list val shared : bool ref val dlcode : bool ref val runtime_variant : string ref + |