diff options
| author | Pierre-Marie Pédrot | 2020-09-03 11:46:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-03 11:46:38 +0200 |
| commit | a2dfddbbda4f410d5bd323e7d4bb95bfcd273a73 (patch) | |
| tree | 7d7fc8162d35a375c607fcc48a7fa1a5e00a00c2 /kernel/vmvalues.ml | |
| parent | 8cd66c83327093ec90f8b7d489cd4bd62d92e5f2 (diff) | |
| parent | 74ea55087202cef48d45705ff3be31e572625cdc (diff) | |
Merge PR #12876: Namegen.visible_ids: fixing what seems to be typos
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/vmvalues.ml')
0 files changed, 0 insertions, 0 deletions