diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-18 01:04:32 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-29 05:11:01 +0200 |
commit | 0c133afc50ccfda19c4952abf579b6d94ab5f229 (patch) | |
tree | 44b52aed6249885748aab7317aad9a3873efcc67 /README.ci.md | |
parent | 778374f081163b4658b8a2efa72cb332179b3a7d (diff) |
Adapting code to renaming Option.fold_map -> Option.fold_left_map.
Diffstat (limited to 'README.ci.md')
0 files changed, 0 insertions, 0 deletions