diff options
Diffstat (limited to 'utils/clflags.mli')
-rw-r--r-- | utils/clflags.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/utils/clflags.mli b/utils/clflags.mli index 5474157c3..97dca6f49 100644 --- a/utils/clflags.mli +++ b/utils/clflags.mli @@ -92,3 +92,4 @@ val runtime_variant : string ref val force_slash : bool ref val keep_locs : bool ref val unsafe_string : bool ref +val opaque : bool ref |