aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMaxime Dénès2017-10-27 18:19:28 +0200
committerMaxime Dénès2017-10-27 18:19:28 +0200
commite5659c8ffe735c530a707a61c692a3af21a79a9a (patch)
tree5f879ecdaea661209c42a863b139eeceb333780e /dev
parentff4793c609d4fc2b868ff673ffaa48abf6d5fa03 (diff)
parentd054ea634f1a586da98753ef197e577c12bf8cfa (diff)
Merge PR #6026: [ocaml] [travis] Add preliminary 4.06 CI testing.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions