diff options
| author | Jason Gross | 2017-06-10 02:56:37 -0400 |
|---|---|---|
| committer | Jason Gross | 2017-06-10 09:50:06 -0400 |
| commit | 5b6aaca42550715300fbd376c2fc0934da554939 (patch) | |
| tree | 438dd5ff004e00e52195f3b13806b4a329990d62 /API/API.mli | |
| parent | a8381e022cf2a967c7c213ec60c5c5252c799332 (diff) | |
Fix Travis sectioning
It drops anything after a `/`, so we change all `/`s into `.`.
There must be a better way to do this that doesn't involve so much bash
hackery, right?
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions