diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-08 23:00:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-08 23:00:23 +0000 |
commit | d8757fb4159e35de9c9a88e0ebb3c2a06d69633d (patch) | |
tree | 78ffba6f0b4e408a900119514300cbed7920aa69 /src/options | |
parent | 480d440174c565bec9aba412c0d35221c9169ff6 (diff) |
Add [*] footnotes to --help output indicating for many options --FOO that there are --no-FOO variants.
Diffstat (limited to 'src/options')
-rwxr-xr-x | src/options/mkoptions | 4 | ||||
-rw-r--r-- | src/options/options_template.cpp | 11 |
2 files changed, 13 insertions, 2 deletions
diff --git a/src/options/mkoptions b/src/options/mkoptions index 540e2b77a..2c514293b 100755 --- a/src/options/mkoptions +++ b/src/options/mkoptions @@ -856,6 +856,10 @@ function doc { the_doc="$the_doc (EXPERTS only)" fi + if [ "$type" = bool -a -n "$long_option" -a "$long_option_alternate" = "no-$long_option" ]; then + the_doc="$the_doc [*]" + fi + doc_line= while [ -n "$the_doc" ]; do remaining_doc="$(expr "$the_doc " : '.\{1,53\} \(.*\)')" diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 560efdfe3..2c1323661 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -226,6 +226,11 @@ Additional CVC4 options:${remaining_documentation}"; #line 228 "${template}" +static const std::string optionsFootnote = "\n\ +[*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\ + sense of the option.\n\ +"; + static const std::string languageDescription = "\ Languages currently supported as arguments to the -L / --lang option:\n\ auto attempt to automatically determine the input language\n\ @@ -248,11 +253,13 @@ std::string Options::getDescription() const { } void Options::printUsage(const std::string msg, std::ostream& out) { - out << msg << optionsDescription << std::endl << std::flush; + out << msg << optionsDescription << std::endl + << optionsFootnote << std::endl << std::flush; } void Options::printShortUsage(const std::string msg, std::ostream& out) { - out << msg << mostCommonOptionsDescription << std::endl << std::endl + out << msg << mostCommonOptionsDescription << std::endl + << optionsFootnote << std::endl << "For full usage, please use --help." << std::endl << std::flush; } |