diff options
| author | Guillaume Melquiond | 2017-09-21 13:41:56 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2017-09-21 13:55:06 +0200 |
| commit | 88c4a5a2958e2c0bbd2d142e684dc642946e2e41 (patch) | |
| tree | c578d50a295d06788e4ef7ca0b41c7c07e7eac93 /API/API.mli | |
| parent | 9933871efd122163f7e2dfe8377b9b2dd384b47b (diff) | |
Handle multiple -w options on command line (bug #5736).
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions