diff options
| author | Emilio Jesus Gallego Arias | 2017-03-14 00:32:53 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-03-14 00:32:53 +0100 |
| commit | addc1304de75800fa9301e97d3ae78539f511959 (patch) | |
| tree | 4c0e9f8244c92206fbfa12761b9a3e7e59a86bb5 /kernel/nativecode.mli | |
| parent | bbae426407ba7df585c22ec687a79c0cf216a6a8 (diff) | |
[library] Refactor state handling.
This part of state is critical. We refactor it and make it into a
record to ease handling.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions