From adfbba6447aa458e95ffad652ba815e080e3b2d3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 8 Sep 2013 23:10:33 -0700
Subject: [PATCH] Fix problem reported by Soonho

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/util/timeit.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/util/timeit.h b/src/util/timeit.h
index 86bfeb6571..d668e6206f 100644
--- a/src/util/timeit.h
+++ b/src/util/timeit.h
@@ -22,7 +22,7 @@ public:
     }
     ~timeit() {
         clock_t end = clock();
-        std::cout << m_msg << " " << ((static_cast<double>(end) - static_cast<double>(m_start)) / CLOCKS_PER_SEC) << " secs\n";
+        m_out << m_msg << " " << ((static_cast<double>(end) - static_cast<double>(m_start)) / CLOCKS_PER_SEC) << " secs\n";
     }
 };
 }