diff options
Diffstat (limited to 'interp/symbols.ml')
| -rw-r--r-- | interp/symbols.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/interp/symbols.ml b/interp/symbols.ml index 3ddb8644f..d1d2d0c84 100644 --- a/interp/symbols.ml +++ b/interp/symbols.ml @@ -589,4 +589,5 @@ let _ = { freeze_function = freeze; unfreeze_function = unfreeze; init_function = init; + survive_module = false; survive_section = false } |