diff options
| author | Son Ho | 2022-11-11 15:10:57 +0100 |
|---|---|---|
| committer | Son HO | 2022-11-11 15:26:17 +0100 |
| commit | 2ad6fec65b0d591da3a2831d4e2c7443f7a22673 (patch) | |
| tree | 093cdee9ebac0513c85cad8b7a2a6377c9d7858c /compiler/dune-project | |
| parent | 411f6964f7d62de6c2b45dfb2400f76686447cd7 (diff) | |
Update the .gitignore
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions