diff options
| author | Hugo Herbelin | 2019-05-08 13:22:34 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 02:31:26 +0200 |
| commit | fe5389542af2d9b6e8d964bbc2c10e997af409fe (patch) | |
| tree | d04d6e75273a7bc55291f5b791ed260a6024eed3 /stm/asyncTaskQueue.mli | |
| parent | 5f3777e9ca29493a242b66f92ba803fa5760a634 (diff) | |
A classification of command line options.
A few semantic changes:
- several queries (-where, -config, ...) are accepted
- queries are exclusive of other arguments
- option -filterops is exclusive of other arguments if it contains
another query (this allows to get rid of the "exitcode" hack)
Diffstat (limited to 'stm/asyncTaskQueue.mli')
0 files changed, 0 insertions, 0 deletions