summaryrefslogtreecommitdiff
path: root/src/options/options_handler.h
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2017-10-10 15:36:09 -0700
committerGitHub <noreply@github.com>2017-10-10 15:36:09 -0700
commitdd979fcdb5a952462e4d6702999b5354de5a7be8 (patch)
treecb4d590f0cba3ec2408633d7e2c70808167b2ad2 /src/options/options_handler.h
parentb7d0c09bd12b9d0f46deab199714ce3441206d7f (diff)
Add copyright information. (#1201)
This adds option --copyright which displays copyright information for CVC4. It further extends --show-config with copyright information and adds a banner with copyright information in interactive mode.
Diffstat (limited to 'src/options/options_handler.h')
-rw-r--r--src/options/options_handler.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 923a87d3a..e534d8e58 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -171,6 +171,7 @@ public:
void notifySetPrintExprTypes(std::string option);
/* main/options_handlers.h */
+ void copyright(std::string option);
void showConfiguration(std::string option);
void showDebugTags(std::string option);
void showTraceTags(std::string option);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback