From d763ea1abfaa2883c94f60cb6c60eedbdea11a56 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 25 May 2016 16:05:39 -0700
Subject: [PATCH] chore(tests/lean/run/IO3): remove unnecessary 'open'

---
 tests/lean/run/IO3.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/tests/lean/run/IO3.lean b/tests/lean/run/IO3.lean
index b9b42c1077..cb261641d0 100644
--- a/tests/lean/run/IO3.lean
+++ b/tests/lean/run/IO3.lean
@@ -1,5 +1,4 @@
 import system.IO
-open string
 
 definition main : IO unit :=
 do { l ← get_line,