diff options
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index e7402cbc6..f9d927f62 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -86,6 +86,7 @@ let _ = { freeze_function = Esyntax.freeze; unfreeze_function = Esyntax.unfreeze; init_function = Esyntax.init; + survive_module = false; survive_section = false } (* Pretty-printing objects = syntax_entry *) @@ -121,6 +122,7 @@ let _ = { freeze_function = Egrammar.freeze; unfreeze_function = Egrammar.unfreeze; init_function = Egrammar.init; + survive_module = false; survive_section = false } (* Tokens *) |