diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-11-02 13:55:48 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-11-02 13:55:48 +0000 |
| commit | b5fd5b61a9f0f993703497fb1c8d678cf2d8bb01 (patch) | |
| tree | 84893172fe9b731e42bf8b5b9103237c06c56252 /src/theory/builtin | |
| parent | d183c7e68eb5b191fcc9d52eaeb86ce1211ba9f7 (diff) | |
Only print a shortlist of most-commonly-used options on option processing errors; reduces clutter, increases usability
Diffstat (limited to 'src/theory/builtin')
0 files changed, 0 insertions, 0 deletions