diff options
| author | Emilio Jesus Gallego Arias | 2017-11-24 18:43:12 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-11-24 22:04:26 +0100 |
| commit | aa560c640eb3f1148c87c4343900138845729105 (patch) | |
| tree | 709db53a99baabbe8f7984396d86128b70dd4f8a /dev/include | |
| parent | c1e670b386f83ed78104a6eb6e4d17cc1d906439 (diff) | |
[lib] Generalize Control.timeout type.
We also remove some internal implementation details from the mli file,
there due historical reasons.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions