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