diff options
| author | Emilio Jesus Gallego Arias | 2017-03-22 01:14:50 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-11-29 14:59:29 +0100 |
| commit | c408e819ce39b27f0842c84b1b24c585ac5b6086 (patch) | |
| tree | a3dac227a23d098e70c7d74bd719f93f3cc6724c /kernel/nativecode.mli | |
| parent | 437f20f0a1c2717cd7baae52e2ab20750dd9d4fb (diff) | |
[lib] [api] Introduce record for `object_prefix`
This is a minor cleanup adding a record in a try to structure the
state living in `Lib`.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions