projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0971930) | patch
Remove `--(no-)interactive-prompt` (#7022)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 19 Aug 2021 23:03:13 +0000 (16:03 -0700)
committerGitHub <noreply@github.com>
Thu, 19 Aug 2021 23:03:13 +0000 (23:03 +0000)
commit51a4feb8f775087fc0a4080978f98346574de50b
tree84cadc958ae96fdfa3fff4fc22d782e0a225340ctree
parent09719301db1532093117bc60546e01dca77b59b8commit | diff
Remove `--(no-)interactive-prompt` (#7022)

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).
src/main/driver_unified.cpp diff | blob | history
src/main/interactive_shell.cpp diff | blob | history
src/options/main_options.toml diff | blob | history