diff options
| author | Théo Zimmermann | 2020-10-19 16:06:30 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-10-20 11:07:52 +0200 |
| commit | 3230c568eb0bc719feca642a1537555e262478eb (patch) | |
| tree | 8d88af13db13ccf36fbe32826e711415c671e93a /kernel/nativecode.ml | |
| parent | 7b07bc9aac0f7f990b8b12e7120d7a4e0bcd4fee (diff) | |
Add some missing smallcaps.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions