diff options
| author | Théo Zimmermann | 2021-01-28 21:18:13 +0100 |
|---|---|---|
| committer | GitHub | 2021-01-28 21:18:13 +0100 |
| commit | ae7b304a5a24816d31fbcef1212e15b98bada7a1 (patch) | |
| tree | d77b45d7c861379cd37d9ce501640914fc489b50 /kernel/nativecode.ml | |
| parent | 639b75a6a5bc2779c684cb8de0042e287c716590 (diff) | |
Apply suggestions from code review
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions