diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-05-09 15:32:38 +0200 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-05-09 15:32:38 +0200 |
commit | b43956fe19177a178dfbcef0b173ebada5060973 (patch) | |
tree | eeebd8b66f92ab5eea48d6708bc3b870bb124f00 /lib/hMap.mli | |
parent | bfa9987d57cd729c40332202a505753beca52e91 (diff) |
Fix typo in configure's option description.
Diffstat (limited to 'lib/hMap.mli')
0 files changed, 0 insertions, 0 deletions