diff options
| author | Ralf Jung | 2017-09-28 16:40:13 +0200 |
|---|---|---|
| committer | Ralf Jung | 2017-09-29 10:56:42 +0200 |
| commit | 39eb1cfb3ac9bc12b6cd80e6bca7c4baf6b365c0 (patch) | |
| tree | 5e0d938a5741edbf02688bb74ce25c2cfaa0845d /API | |
| parent | 4b6383889d4d38de4c9a28bee960b30114a51b16 (diff) | |
Iris CI: use opam to determine std++ git commit
Diffstat (limited to 'API')
0 files changed, 0 insertions, 0 deletions