diff options
| author | Emilio Jesus Gallego Arias | 2017-03-22 21:26:25 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-03-23 00:16:04 +0100 |
| commit | f58df8669c60dfdc6092810da13707cb965cf151 (patch) | |
| tree | afad4370307ef73da6ac75f1bc4f6721c39f5bc9 /lib/future.ml | |
| parent | 8b73fd7c6ce423f8c8a2594e90200f2407795d52 (diff) | |
[META] add support for ide libraries
This makes sense for clients willing to link to richpp.
Diffstat (limited to 'lib/future.ml')
0 files changed, 0 insertions, 0 deletions