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 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 |