diff options
| author | Maxime Dénès | 2018-12-21 11:43:56 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-21 11:45:26 +0100 |
| commit | cc72a78df3ef850cb09680ae0d9f90aa4cc91861 (patch) | |
| tree | ef52a41c8a05b9224f23656bb81bc290213d0a73 /doc/plugin_tutorial/tuto1/src/simple_check.ml | |
| parent | ba6b5839add7587837b4cea890f2d505ce76d489 (diff) | |
Do not exclude "opened" bugs from report
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_check.ml')
0 files changed, 0 insertions, 0 deletions