diff options
author | Gabriel Scherer <gabriel.scherer@gmail.com> | 2013-08-04 19:58:09 +0000 |
---|---|---|
committer | Gabriel Scherer <gabriel.scherer@gmail.com> | 2013-08-04 19:58:09 +0000 |
commit | b1c5fa3e5260e8b1d5acb21a93fdcb826627391c (patch) | |
tree | 28e7e0ff0bd206f70ccb5666ff6655fd7b76dc1a /utils/clflags.ml | |
parent | da3011fec235bb5bbecbefc11b247bc28a840195 (diff) |
PR#6071: Add a -noinit option to the toplevel [patch by David Sheets]
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@13972 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
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 *) - |