diff --git a/src/library/io_state.cpp b/src/library/io_state.cpp
index 89123361c1..7fbe2d58be 100644
--- a/src/library/io_state.cpp
+++ b/src/library/io_state.cpp
@@ -194,6 +194,8 @@ set_io_state::~set_io_state() {
     lua_settable(m_state, LUA_REGISTRYINDEX);
     if (!m_prev)
         set_global_options(m_state, m_prev_options);
+    else
+        set_global_options(m_state, m_prev->get_options());
 }
 
 io_state * get_io_state(lua_State * L) {
diff --git a/tests/lean/lua17.lean b/tests/lean/lua17.lean
new file mode 100644
index 0000000000..d0c9c61d06
--- /dev/null
+++ b/tests/lean/lua17.lean
@@ -0,0 +1,14 @@
+
+Variables a b : Int
+Show Options
+(**
+  local ios = io_state()
+
+  print(get_options())
+  print(get_options())
+  ios:print(parse_lean("a + b"))
+  print(parse_lean("fun x, a + x"))
+  print(get_options())
+**)
+Show Options
+Show Environment 2
\ No newline at end of file
diff --git a/tests/lean/lua17.lean.expected.out b/tests/lean/lua17.lean.expected.out
new file mode 100644
index 0000000000..10c8b08d4e
--- /dev/null
+++ b/tests/lean/lua17.lean.expected.out
@@ -0,0 +1,13 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: a
+  Assumed: b
+⟨pp::unicode ↦ true, pp::colors ↦ false⟩
+⟨pp::unicode ↦ true, pp::colors ↦ false⟩
+⟨pp::unicode ↦ true, pp::colors ↦ false⟩
+Int::add a b
+λ x : ℤ, a + x
+⟨pp::unicode ↦ true, pp::colors ↦ false⟩
+⟨pp::unicode ↦ true, pp::colors ↦ false⟩
+Variable a : ℤ
+Variable b : ℤ