From f60dbe5eb60895a1d7f4606dcb4d4459fcfce955 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 1 Feb 2016 11:10:51 -0800 Subject: [PATCH] Making the ManagedOstream::defaultSource() a const function. --- src/smt/managed_ostreams.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h index 05d026b24..6dc785027 100644 --- a/src/smt/managed_ostreams.h +++ b/src/smt/managed_ostreams.h @@ -48,7 +48,7 @@ class ManagedOstream { void set(const std::string& filename); /** If this is associated with an option, return the string value. */ - virtual std::string defaultSource() { return ""; } + virtual std::string defaultSource() const { return ""; } protected: -- 2.30.2