diff options
| author | Son Ho | 2022-02-01 19:14:54 +0100 |
|---|---|---|
| committer | Son Ho | 2022-02-01 19:14:54 +0100 |
| commit | da9fc439f332d96a86aaf8e3b07eca6798f860fe (patch) | |
| tree | 5b1bf28cf2cb84b64293adf9dc2590b7ad1f79e5 /src/Identifiers.ml | |
| parent | c70d13bcd11614833875169f641deb215a0eef1e (diff) | |
Introduce a small optimization
Diffstat (limited to 'src/Identifiers.ml')
0 files changed, 0 insertions, 0 deletions