diff options
| author | Hugo Herbelin | 2018-09-26 14:30:47 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-27 13:28:36 +0200 |
| commit | 4865687c8c5641170080a47c72ee26c75eece49d (patch) | |
| tree | 5643372d9537c095c975e5bd904dac6a1a68c9b0 /kernel/nativecode.ml | |
| parent | 9afe18c3190bb0210e03bf40f3af101a7c5604da (diff) | |
Using Constant.change_label (better level of abstraction to build kernel names).
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions