diff options
Diffstat (limited to 'utils')
| -rw-r--r-- | utils/clflags.ml | 2 | ||||
| -rw-r--r-- | utils/clflags.mli | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/utils/clflags.ml b/utils/clflags.ml index 516ea8f29..cda46bd2e 100644 --- a/utils/clflags.ml +++ b/utils/clflags.ml @@ -33,7 +33,7 @@ and ccopts = ref ([] : string list) (* -ccopt *) and classic = ref false (* -nolabels *) and nopervasives = ref false (* -nopervasives *) and preprocessor = ref(None : string option) (* -pp *) -let save_types = ref false (* -stypes *) +let annotations = ref false (* -annot *) and use_threads = ref false (* -thread *) and use_vmthreads = ref false (* -vmthread *) and noassert = ref false (* -noassert *) diff --git a/utils/clflags.mli b/utils/clflags.mli index 0dcbaddf9..728cd285c 100644 --- a/utils/clflags.mli +++ b/utils/clflags.mli @@ -30,7 +30,7 @@ val ccopts : string list ref val classic : bool ref val nopervasives : bool ref val preprocessor : string option ref -val save_types : bool ref +val annotations : bool ref val use_threads : bool ref val use_vmthreads : bool ref val noassert : bool ref |