diff --git a/src/library/io_state.cpp b/src/library/io_state.cpp index 5bf587e97..f5223ff79 100644 --- a/src/library/io_state.cpp +++ b/src/library/io_state.cpp @@ -20,6 +20,12 @@ io_state::io_state(options const & opts, formatter const & fmt): m_regular_channel(std::make_shared()), m_diagnostic_channel(std::make_shared()) { } +io_state::io_state(io_state const & ios, std::shared_ptr const & r, std::shared_ptr const d): + m_options(ios.m_options), + m_formatter(ios.m_formatter), + m_regular_channel(r), + m_diagnostic_channel(d) { +} io_state::~io_state() {} diff --git a/src/library/io_state.h b/src/library/io_state.h index 8a6d490ff..ebe31c69a 100644 --- a/src/library/io_state.h +++ b/src/library/io_state.h @@ -25,6 +25,7 @@ class io_state { public: io_state(formatter const & fmt); io_state(options const & opts, formatter const & fmt); + io_state(io_state const & ios, std::shared_ptr const & r, std::shared_ptr const d); ~io_state(); options get_options() const { return m_options; }