diff options
Diffstat (limited to 'interp/reserve.ml')
-rw-r--r-- | interp/reserve.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/interp/reserve.ml b/interp/reserve.ml index d2c84abdf..dc7393c67 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -21,6 +21,7 @@ let _ = { Summary.freeze_function = (fun () -> !reserve_table); Summary.unfreeze_function = (fun r -> reserve_table := r); Summary.init_function = (fun () -> reserve_table := Idmap.empty); + Summary.survive_module = false; Summary.survive_section = false } let declare_reserved_type id t = |