aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/future.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-13 11:33:48 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-13 11:33:48 +0100
commitecacc9af6100f76e95acc24e777026bfc9c4d921 (patch)
tree4c319de83cb07833fb253b2c3cd68d8a882c639b /lib/future.ml
parente2135c2f5fd8846c30d8099eed523fe06202b614 (diff)
parentfd5c5da475baea11d7ee2e1c2e965d7faeed3f33 (diff)
Merge PR#456: Proposing improvement to the CI targets for local use
Diffstat (limited to 'lib/future.ml')
0 files changed, 0 insertions, 0 deletions