diff options
| author | Ben Lee-Cohen | 2022-05-04 02:17:08 +0000 |
|---|---|---|
| committer | GitHub | 2022-05-04 02:17:08 +0000 |
| commit | 09a17e4fa3d0aa67e399c02c484a768d85acaac6 (patch) | |
| tree | 60f097b309ee1897f150ccf321239b4f71b841b7 /runtime/queries/lean | |
| parent | f59b3b91c86d8f92ce72a4bb873bbb6aaaa4d2a9 (diff) | |
Making the 'set-option' command help more descriptive. (#2365)
* Making the 'set-option' command help more descriptive.
* Adding the generated docs
* Making the message multi-line
* Replace newline with break in generated docs
Diffstat (limited to 'runtime/queries/lean')
0 files changed, 0 insertions, 0 deletions