diff options
Diffstat (limited to 'utils/clflags.ml')
| -rw-r--r-- | utils/clflags.ml | 2 |
1 files changed, 1 insertions, 1 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 *) |