diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-06 16:26:04 +0100 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-06 16:26:04 +0100 |
commit | 905e3dd364e8be20771c39393e7e114f2e4b8cd8 (patch) | |
tree | 543259622569f4fafb2a8b19b25b4b6abd18ac38 /checker | |
parent | 8b5d02d8706f99015c2ce8efcad32b7af228dd53 (diff) |
Fix description of command-line options in the manual.
Diffstat (limited to 'checker')
0 files changed, 0 insertions, 0 deletions