diff options
| author | Emilio Jesus Gallego Arias | 2019-07-03 13:02:55 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-03 13:02:55 +0200 |
| commit | 465ee008d15bb1fb0428aef513b8c3fd3456327a (patch) | |
| tree | dfc870d1a5d7b6d50adbd25e805f9521143a10a0 /kernel/names.ml | |
| parent | 60a13c4f6f9ce211a4078634e66d5eae49035ccc (diff) | |
| parent | e49ecf90e565b9e49f114cadb6b24ab660cd02f3 (diff) | |
Merge PR #10338: Fix #9455: avoid update_global_env when unchanged Global.universes()
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Ack-by: gares
Diffstat (limited to 'kernel/names.ml')
0 files changed, 0 insertions, 0 deletions