diff options
| author | Son Ho | 2021-11-03 12:04:57 +0100 |
|---|---|---|
| committer | Son Ho | 2021-11-03 12:04:57 +0100 |
| commit | b582131d54a41a707c4ab75c3bc03251601fb230 (patch) | |
| tree | dc72d71a86b4dbfecb4be77e47c489477154ba78 /.gitignore | |
| parent | 47a8983a5e95e306bddbcf031777ad781479fdd8 (diff) | |
Split main.ml between Identifiers.ml and Types.ml
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions