diff options
| author | Tim King <taking@google.com> | 2016-02-01 11:10:51 -0800 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2016-02-01 11:10:51 -0800 |
| commit | f60dbe5eb60895a1d7f4606dcb4d4459fcfce955 (patch) | |
| tree | da9d69c9a4ceccf893b443a351fa9bbe2afdcea6 /src | |
| parent | b89545b4d9b235f8b66b8558a24bdd20d20f3dea (diff) | |
Making the ManagedOstream::defaultSource() a const function.
Diffstat (limited to 'src')
| -rw-r--r-- | src/smt/managed_ostreams.h | 2 |
1 files changed, 1 insertions, 1 deletions
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: |