diff options
| author | Théo Zimmermann | 2020-11-13 09:20:21 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-11-13 09:20:21 +0100 |
| commit | 53aa272821c2cd94e4b05382fa33449e851c7a90 (patch) | |
| tree | e7e52529768d9d85a1d99c89517a6b9fad390387 /doc/plugin_tutorial/tuto2/src | |
| parent | 51e759fb2ff92dd89ab4823ddea3ea81be7f8046 (diff) | |
Fix dune rules for @check-gram following recent changes.
Diffstat (limited to 'doc/plugin_tutorial/tuto2/src')
0 files changed, 0 insertions, 0 deletions