diff options
| author | Gaëtan Gilbert | 2019-06-07 15:42:39 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-12 14:00:05 +0200 |
| commit | e49ecf90e565b9e49f114cadb6b24ab660cd02f3 (patch) | |
| tree | e93b6b46a5458d02b974c87a44410f39b34d9d76 /plugins/extraction | |
| parent | 0d4300771e4a6a26d948872262a79695a38c7e0d (diff) | |
Fix #9455: avoid update_global_env when unchanged Global.universes()
This also makes vernacentries correct wrt update_global_env.
Diffstat (limited to 'plugins/extraction')
0 files changed, 0 insertions, 0 deletions