diff options
| author | Théo Zimmermann | 2020-09-27 12:31:14 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-09-27 12:31:14 +0200 |
| commit | c571af2f95cccfbffe4e0b93525066676e7f652d (patch) | |
| tree | 68d4f8fd36d03482d2a33ee5e64d5ff813ebbe2c /doc/plugin_tutorial/tuto3/src/dune | |
| parent | 9c2228ff011dc6188b70084fa1e1a5158affcf24 (diff) | |
Reduce nitpick_ignore list a little.
Diffstat (limited to 'doc/plugin_tutorial/tuto3/src/dune')
0 files changed, 0 insertions, 0 deletions