diff options
| author | Gaëtan Gilbert | 2019-10-28 15:08:31 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-28 15:08:31 +0100 |
| commit | 9297352202fa6a43faf266a97a6a07d1df317b9a (patch) | |
| tree | 6f1919e823acc91bffbe53d5c2065a038df86c91 /kernel/nativecode.mli | |
| parent | b5d1c31e2d10084935d36a67e0d44b725210b979 (diff) | |
| parent | 252aaae6a6955718609a94b7ae5ac707145d5064 (diff) | |
Merge PR #10952: [library] [nit] Remove unnecessary type alias.
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions