diff options
author | Chimrod <> | 2023-09-27 15:36:13 +0200 |
---|---|---|
committer | Chimrod <> | 2023-09-29 10:00:21 +0200 |
commit | 5dc0c5defdd7ebb152a00e8b2895787b54931779 (patch) | |
tree | 78f9d7c646d3c614a6c934778b195e0707f47821 /syntax/tree.mli | |
parent | 40f7b4c7398db2b832b71e3dfb8afb53116fad51 (diff) |
Allow differents file encoding for the source
Diffstat (limited to 'syntax/tree.mli')
0 files changed, 0 insertions, 0 deletions