summaryrefslogtreecommitdiff
path: root/src/main/interactive_shell.h
diff options
context:
space:
mode:
authorGereon Kremer <nafur42@gmail.com>2021-08-27 11:23:15 -0700
committerGitHub <noreply@github.com>2021-08-27 18:23:15 +0000
commit3183ca6685f6b0dcca538efb72e6840a56479b60 (patch)
treee6c51d6175d4a56c7849aa4f965ed49b743f0607 /src/main/interactive_shell.h
parenta698b522d619c800a3401c7294cf1c6c663d7acc (diff)
Handle languages as strings in driver (#7074)
This PR moves the first chunk of code in the driver to use the proper options API for the language options. It is now handled as a string.
Diffstat (limited to 'src/main/interactive_shell.h')
-rw-r--r--src/main/interactive_shell.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index cf5f22b51..d4736470f 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -40,7 +40,7 @@ class SymbolManager;
class InteractiveShell
{
- const Options& d_options;
+ api::Solver* d_solver;
std::istream& d_in;
std::ostream& d_out;
parser::Parser* d_parser;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback