diff options
| author | Emilio Jesus Gallego Arias | 2018-11-07 13:55:14 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-07 13:56:12 +0100 |
| commit | 6cc40e73879aec50227c9576100a381cc11ade30 (patch) | |
| tree | f8ca5d6e658e20660ff973a98574e83f9e90f427 /doc/plugin_tutorial/tuto1/src/simple_declare.ml | |
| parent | f8b340ee5d1adce859f5b394c736f7cd60e0b9fb (diff) | |
[warnings] Fix couple of warnings related to API..
Changes in declare following @SkySkimmer's advice.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_declare.ml')
0 files changed, 0 insertions, 0 deletions