diff options
author | 2018-06-13 10:21:30 +0200 | |
---|---|---|
committer | 2018-06-13 10:21:30 +0200 | |
commit | 573c6d76d343cadaa68b5851fdebba937153c24d (patch) | |
tree | 8e1d4553d6f0453132e52acc80d20ab6f4dad2c9 /kernel/names.mli | |
parent | 7e7aa7491e3743abe858c1be6b77bd9a986d4297 (diff) | |
parent | 3551dd18f515e0fbf114708ea64e5c3662124093 (diff) |
Merge PR #7782: [VM] Rename reloc -> cenv
Diffstat (limited to 'kernel/names.mli')
0 files changed, 0 insertions, 0 deletions