diff options
| author | Jim Fehrle | 2018-09-01 12:39:09 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2018-09-20 18:27:08 -0700 |
| commit | ec7dd674ea25dfd36c007bb863fed63ce8d31ff2 (patch) | |
| tree | 2f73dd477ac9276ba8ed9409aab613370d29c7fb /library/goptions.ml | |
| parent | d4b5de427d94d82f09d58e0f1095f052a5900914 (diff) | |
Rewrite "Flags, Options and Tables" section.
Mark boolean-valued options with :flag:
Adjust tactic and command names so parameters aren't shown in the index unless
they're needed for disambiguation.
Remove references to synchronous options.
Revise doc for tables.
Correct indentation for text below :flag:
Diffstat (limited to 'library/goptions.ml')
| -rw-r--r-- | library/goptions.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index eafcb8fea6..dcbc46ab72 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -412,7 +412,7 @@ let print_tables () = if depr then msg ++ str " [DEPRECATED]" ++ fnl () else msg ++ fnl () in - str "Synchronous options:" ++ fnl () ++ + str "Options:" ++ fnl () ++ OptionMap.fold (fun key (name, depr, (read,_,_)) p -> p ++ print_option key name (read ()) depr) |