diff options
| author | Yves Bertot | 2018-11-07 08:21:02 +0100 |
|---|---|---|
| committer | GitHub | 2018-11-07 08:21:02 +0100 |
| commit | a5116a4ad9689af0906e463786f2a5ccca4a35be (patch) | |
| tree | 7e39439474c42a2ccc80de1cfe87fb808952513b /doc/plugin_tutorial/tuto1/src/simple_check.mli | |
| parent | a3e1acb50be3b700b7c36daef4d56f6c6d3ded6a (diff) | |
| parent | 9e5447b196804fd9ce754931e21802e5d02031d9 (diff) | |
Merge pull request #15 from ejgallego/add_travis
[travis] Add Travis File.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_check.mli')
0 files changed, 0 insertions, 0 deletions