aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-17 23:29:06 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-17 23:29:06 +0100
commit0b53955bb2bec43454ccbd317a09787a24fff3ae (patch)
tree7e341e81e6f527b9271640222e1cc926677d08cb
parenta91df5fdc60977accd7937eb17b62bd551d3213a (diff)
Deprecated options issue a warning.
-rw-r--r--library/goptions.ml10
1 files changed, 7 insertions, 3 deletions
diff --git a/library/goptions.ml b/library/goptions.ml
index 4aea33685..ef25fa590 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -268,10 +268,14 @@ let declare_option cast uncast
begin fun v -> add_anonymous_leaf (gdecl_obj v) end
else write,write,write
in
+ let warn () =
+ if depr then
+ msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated")
+ in
let cread () = cast (read ()) in
- let cwrite v = write (uncast v) in
- let clwrite v = lwrite (uncast v) in
- let cgwrite v = gwrite (uncast v) in
+ let cwrite v = warn (); write (uncast v) in
+ let clwrite v = warn (); lwrite (uncast v) in
+ let cgwrite v = warn (); gwrite (uncast v) in
value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,clwrite,cgwrite)) !value_tab;
write