diff options
| author | Pierre Roux | 2020-09-07 11:53:49 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-09-11 22:20:28 +0200 |
| commit | 724966f56caa66a5ddc9a992cf870ebc2efae004 (patch) | |
| tree | 53954c47fd9e400d1e6006d38472c0b858893303 /kernel/genOpcodeFiles.ml | |
| parent | 754e138e1e1c86dcd5e9d07084a5d33a5056ce9d (diff) | |
[refman] Rename int to integer
Diffstat (limited to 'kernel/genOpcodeFiles.ml')
0 files changed, 0 insertions, 0 deletions