diff options
| author | Chimrod <> | 2023-10-03 08:43:52 +0200 |
|---|---|---|
| committer | Chimrod <> | 2023-10-03 08:43:52 +0200 |
| commit | ea509dd21ebec0ecb4f307d9786ca75dc03eab75 (patch) | |
| tree | 258600d8da252aa25c627eb8d90fc09a48496ebc /tools/dune | |
| parent | c7683b81be07f76ab8f1bfb95273291720eb017c (diff) | |
Added a small report indicating the number of errors and warning
Diffstat (limited to 'tools/dune')
0 files changed, 0 insertions, 0 deletions