diff options
| author | Hugo Herbelin | 2016-07-12 23:26:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-05 17:49:22 +0200 |
| commit | 7e28feadd6394483b6f527d5aed7d663e189596e (patch) | |
| tree | 9068e370691fa50b37668487268abcde0c0e430d /dev | |
| parent | cff6f53cbef53ce3902e59853f7a7dc9b7150f45 (diff) | |
Upgrading some local function as a general-purpose combinator Option.List.map.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions