diff options
| author | Théo Zimmermann | 2017-10-05 11:21:59 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2017-10-05 11:22:26 +0200 |
| commit | ae0d9d3bc64171de60ccc6754b5836a89190a601 (patch) | |
| tree | 1a71105dc78eb02cc26e1472b338f517c7e4ec6c /API/API.mli | |
| parent | 2b9a34e2ffb2bf066b3b0f8452e35622519cae1c (diff) | |
[ci] Remove deploy to GitHub of OS X package.
This is inconvenient because it can only be tested on tags
and it didn't work for V8.7+beta1.
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions