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 4ff808f33..7a40afe42 100644 --- a/utils/clflags.ml +++ b/utils/clflags.ml @@ -42,6 +42,7 @@ and verbose = ref false (* -verbose *) and noprompt = ref false (* -noprompt *) and nopromptcont = ref false (* -nopromptcont *) and init_file = ref (None : string option) (* -init *) +and noinit = ref false (* -noinit *) and use_prims = ref "" (* -use-prims ... *) and use_runtime = ref "" (* -use-runtime ... *) and principal = ref false (* -principal *) @@ -101,4 +102,3 @@ let shared = ref false (* -shared *) let dlcode = ref true (* not -nodynlink *) let runtime_variant = ref "";; (* -runtime-variant *) - |