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