From 04f12ad8b6f94d952b54f433bbf32eaa481d006b Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 26 Nov 2013 16:36:29 -0500
Subject: [PATCH] Fix Java output stream adapter.

---
 src/bindings/java_stream_adapters.h | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

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 {
-- 
2.30.2