From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 26 Nov 2013 21:36:29 +0000 (-0500)
Subject: Fix Java output stream adapter.
X-Git-Tag: cvc5-1.0.0~7241
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=04f12ad8b6f94d952b54f433bbf32eaa481d006b;p=cvc5.git

Fix Java output stream adapter.
---

diff --git a/src/bindings/java_stream_adapters.h b/src/bindings/java_stream_adapters.h
index eefb31e6d..f3546613c 100644
--- a/src/bindings/java_stream_adapters.h
+++ b/src/bindings/java_stream_adapters.h
@@ -42,14 +42,9 @@
 
 namespace CVC4 {
 
-class JavaOutputStreamAdapter {
-  std::stringstream d_ss;
-
+class JavaOutputStreamAdapter : public std::ostringstream {
 public:
-  JavaOutputStreamAdapter() { }
-
-  std::string toString() { return d_ss.str(); }
-
+  std::string toString() { return str(); }
 };/* class JavaOutputStreamAdapter */
 
 class JavaInputStreamAdapter : public std::stringstream {