diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-08-16 23:39:38 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2021-08-16 23:39:38 -0700 |
commit | 68d7289ab38f0381bed60ee852175f26bb20d1d2 (patch) | |
tree | 21b04c1ed9e00f87f35cde8f5004161ff813ccb1 /src/prop/cnf_stream.h | |
parent | df8caeeb9490ba712744f814ba92916a8ae4ab1e (diff) |
Remove `--(no-)interactive-prompt`
This option is mostly redundant: It offers a way to access the
interactive shell without any copyright information or `cvc5>` prompt
being printed. However, `--no-interactive` offers the same experience
(except for the features offered by libedit).
Diffstat (limited to 'src/prop/cnf_stream.h')
0 files changed, 0 insertions, 0 deletions