diff options
Diffstat (limited to 'utils')
| -rw-r--r-- | utils/clflags.ml | 2 | ||||
| -rw-r--r-- | utils/clflags.mli | 1 |
2 files changed, 2 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 *) - diff --git a/utils/clflags.mli b/utils/clflags.mli index e67113363..ad2ce36a9 100644 --- a/utils/clflags.mli +++ b/utils/clflags.mli @@ -39,6 +39,7 @@ val verbose : bool ref val noprompt : bool ref val nopromptcont : bool ref val init_file : string option ref +val noinit : bool ref val use_prims : string ref val use_runtime : string ref val principal : bool ref |