diff options
| author | Kazuhiko Sakaguchi | 2019-06-06 16:05:52 +0200 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2019-06-06 16:19:08 +0200 |
| commit | 8c53c2909511a6ff324ac39bb0ff1040c04de712 (patch) | |
| tree | 5b1e0907869dc7ea6fd872bea4e7fe388bbfc7f7 /doc/plugin_tutorial/tuto1/src/simple_check.ml | |
| parent | 4f7af2b09a935528d660a354f5e7672fc92e9a5c (diff) | |
Update changes.rst as a follow-up to #9743
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_check.ml')
0 files changed, 0 insertions, 0 deletions