diff options
| author | Hugo Herbelin | 2019-11-11 15:48:08 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-22 16:44:50 +0200 |
| commit | 74ea55087202cef48d45705ff3be31e572625cdc (patch) | |
| tree | 3dac103f72e088f3e6d71060a9e016c2cf70052c /kernel/nativevalues.mli | |
| parent | f149d617b631d6fc64937d3882ed3db16fdf6c8f (diff) | |
Namegen.visible_ids: fixing what seems to be typos.
Diffstat (limited to 'kernel/nativevalues.mli')
0 files changed, 0 insertions, 0 deletions