diff options
Diffstat (limited to 'library/goptions.mli')
| -rw-r--r-- | library/goptions.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/library/goptions.mli b/library/goptions.mli index 1a89961ac..37c03f1bf 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -117,8 +117,13 @@ module MakeRefTable : type 'a option_sig = { optsync : bool; + (** whether the option is synchronous w.r.t to the section/module system. *) + optdepr : bool; + (** whether the option is DEPRECATED *) optname : string; + (** a short string describing the option *) optkey : option_name; + (** the low-level name of this option *) optread : unit -> 'a; optwrite : 'a -> unit } |