summaryrefslogtreecommitdiffstats
path: root/utils/clflags.ml
diff options
context:
space:
mode:
authorGabriel Scherer <gabriel.scherer@gmail.com>2013-08-04 19:58:09 +0000
committerGabriel Scherer <gabriel.scherer@gmail.com>2013-08-04 19:58:09 +0000
commitb1c5fa3e5260e8b1d5acb21a93fdcb826627391c (patch)
tree28e7e0ff0bd206f70ccb5666ff6655fd7b76dc1a /utils/clflags.ml
parentda3011fec235bb5bbecbefc11b247bc28a840195 (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.ml2
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 *)
-