diff options
| author | Théo Zimmermann | 2020-11-09 16:34:39 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-11-09 16:42:02 +0100 |
| commit | 3f5f5cf07de6eb804e52da8213a0f1a75cb0cdbe (patch) | |
| tree | f3a976146d19c349b310d7f468ddedbb1a357fc3 /kernel/nativecode.mli | |
| parent | c0b48997dc7fccd15ab237df6274dbcfa05cbc9c (diff) | |
Fix #5226: Add index entry for ::=.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions