diff options
Diffstat (limited to 'library/goptions.ml')
| -rw-r--r-- | library/goptions.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index 73132868d7..1418407533 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -90,7 +90,7 @@ module MakeTable = let inGo : option_mark * A.t -> obj = Libobject.declare_object {(Libobject.default_object nick) with Libobject.load_function = load_options; - Libobject.open_function = load_options; + Libobject.open_function = simple_open load_options; Libobject.cache_function = cache_options; Libobject.subst_function = subst_options; Libobject.classify_function = (fun x -> Substitute x)} @@ -262,7 +262,7 @@ let declare_option cast uncast append ?(preprocess = fun x -> x) declare_object { (default_object (nickname key)) with load_function = load_options; - open_function = open_options; + open_function = simple_open open_options; cache_function = cache_options; subst_function = subst_options; discharge_function = discharge_options; |