From ef60e6abd23629f21344a23d794c2950666bfcc2 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Tue, 21 Oct 2014 17:21:48 -0700 Subject: [PATCH] fix(shell/lean.cpp): use temp ios --- src/shell/lean.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 87e6f8e8cd..7ed6e8519c 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -269,7 +269,8 @@ public: bool ok = true; try { environment temp_env(env); - if (!parse_commands(temp_env, ios, input_filename.c_str(), false, num_threads)) { + io_state temp_ios(ios); + if (!parse_commands(temp_env, temp_ios, input_filename.c_str(), false, num_threads)) { ok = false; } } catch (lean::exception & ex) {