summaryrefslogtreecommitdiff
path: root/src/smt/managed_ostreams.cpp
diff options
context:
space:
mode:
authorGereon Kremer <nafur42@gmail.com>2021-05-29 09:09:34 +0200
committerGitHub <noreply@github.com>2021-05-29 07:09:34 +0000
commit0133367f9ed242aa01e42867364c7be74ffe5618 (patch)
tree993330d559b7d86f0b891792cde07dc1a4c8bc8c /src/smt/managed_ostreams.cpp
parentf62b46414cc47762857a4e3241318733ca8c973d (diff)
Remove `Options::set()` method (#6556)
This PR gets rid of the Options::set() method, replacing it by direct access to the options data. This method was only used internally and did nothing except for resolving the options data from the option tag type via template specializations (via ref()), which is no longer necessary.
Diffstat (limited to 'src/smt/managed_ostreams.cpp')
-rw-r--r--src/smt/managed_ostreams.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp
index ee356e413..b09448c11 100644
--- a/src/smt/managed_ostreams.cpp
+++ b/src/smt/managed_ostreams.cpp
@@ -91,7 +91,7 @@ ManagedRegularOutputChannel::~ManagedRegularOutputChannel() {
// to null_os. Consult RegularOutputChannelListener for the list of
// channels.
if(options::err() == getManagedOstream()){
- Options::current().set(options::err, &null_os);
+ Options::current().base.err = &null_os;
}
}
@@ -115,7 +115,7 @@ ManagedDiagnosticOutputChannel::~ManagedDiagnosticOutputChannel() {
// to null_os. Consult DiagnosticOutputChannelListener for the list of
// channels.
if(options::err() == getManagedOstream()){
- Options::current().set(options::err, &null_os);
+ Options::current().base.err = &null_os;
}
if(Debug.getStreamPointer() == getManagedOstream()) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback