diff options
| author | Emilio Jesus Gallego Arias | 2017-11-19 04:47:15 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-11-19 04:51:49 +0100 |
| commit | a554519874c15d0a790082e5f15f3dc2419c6c38 (patch) | |
| tree | fbca74c97943685e93e10b85de708cc7c54a7abe /API/API.mli | |
| parent | edf1a8f36f75861b822081b3825357e122b6937d (diff) | |
[lib] Minor pending cleanup to consolidate helper function.
While we are at it we refactor a few special cases of the helper.
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions