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 /.gitignore | |
| parent | bfa9987d57cd729c40332202a505753beca52e91 (diff) | |
Fix typo in configure's option description.
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions