diff options
| author | Christian Doczkal | 2018-12-09 14:01:06 +0100 |
|---|---|---|
| committer | GitHub | 2018-12-09 14:01:06 +0100 |
| commit | c6f998985813b1eb91e909d7d7408bc3e44f9d3b (patch) | |
| tree | 2964461066169aafe6754255baecc297f400e099 /doc/plugin_tutorial/tuto1/src/simple_check.ml | |
| parent | 9f33dc1ac4e06c0bda64fa817cb3fbbbb56cc0b1 (diff) | |
fix copy-paste error in CI_ARCHIVEURL
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_check.ml')
0 files changed, 0 insertions, 0 deletions