diff options
| author | Hugo Herbelin | 2020-02-11 22:30:36 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-11 22:34:04 +0100 |
| commit | 6884867957d1cc361030cffd18d24cb8a231dd10 (patch) | |
| tree | 90edbcd57b1971bdd1237ef065cd7c2123c79892 /kernel/typeops.mli | |
| parent | cbf5e7e49cfa243b6eac808241894fc504d84e5f (diff) | |
Fixing extra space in "Print Grammar" (i.e. Grammar.Entry.print in Gramlib).
Diffstat (limited to 'kernel/typeops.mli')
0 files changed, 0 insertions, 0 deletions