diff options
| author | Hugo Herbelin | 2020-08-22 12:50:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-28 15:34:00 +0200 |
| commit | 1a91771fdc26bd0260ff26aceb91070217717d3b (patch) | |
| tree | 0aec8f289eb7da44dfb1e38f205282ebbc2804aa /kernel/nativecode.mli | |
| parent | 699eb941cbdd2b3caf98f18b2d49b249b598ca1b (diff) | |
When printing the type in About, use the renamed arguments.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions