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