diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-13 10:21:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-13 10:21:30 +0200 |
| commit | 573c6d76d343cadaa68b5851fdebba937153c24d (patch) | |
| tree | 8e1d4553d6f0453132e52acc80d20ab6f4dad2c9 /kernel/names.ml | |
| parent | 7e7aa7491e3743abe858c1be6b77bd9a986d4297 (diff) | |
| parent | 3551dd18f515e0fbf114708ea64e5c3662124093 (diff) | |
Merge PR #7782: [VM] Rename reloc -> cenv
Diffstat (limited to 'kernel/names.ml')
0 files changed, 0 insertions, 0 deletions