diff options
Diffstat (limited to 'src/main/options.h')
| -rw-r--r-- | src/main/options.h | 15 |
1 files changed, 3 insertions, 12 deletions
diff --git a/src/main/options.h b/src/main/options.h index 832abcf9d..d3af4994d 100644 --- a/src/main/options.h +++ b/src/main/options.h @@ -25,19 +25,10 @@ namespace cvc5::main { /** - * Print overall command-line option usage message, prefixed by - * "msg"---which could be an error message causing the usage - * output in the first place, e.g. "no such option --foo" + * Print overall command-line option usage message to the given output stream + * with binary being the command to run cvc5. */ -void printUsage(const std::string& msg, std::ostream& os); - -/** - * Print command-line option usage message for only the most-commonly - * used options. The message is prefixed by "msg"---which could be - * an error message causing the usage output in the first place, e.g. - * "no such option --foo" - */ -void printShortUsage(const std::string& msg, std::ostream& os); +void printUsage(const std::string& binary, std::ostream& os); /** * Initialize the Options object options based on the given |