diff options
Diffstat (limited to 'library/goptions.ml')
| -rw-r--r-- | library/goptions.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index 1b29721c1..111448cf1 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -88,6 +88,7 @@ module MakeTable = { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init; + Summary.survive_module = false; Summary.survive_section = true } let (add_option,remove_option) = @@ -250,6 +251,7 @@ let declare_option cast uncast {freeze_function = read; unfreeze_function = write; init_function = (fun () -> write default); + survive_module = false; survive_section = true} in fun v -> add_anonymous_leaf (decl_obj v) |