diff --git a/tests/lean/interactive/config.lean.expected.out b/tests/lean/interactive/config.lean.expected.out
index 0efee9e48..6b642d82c 100644
--- a/tests/lean/interactive/config.lean.expected.out
+++ b/tests/lean/interactive/config.lean.expected.out
@@ -1,4 +1,3 @@
-Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
 #   Set: pp::colors
   Set: pp::unicode
   Set: pp::colors
diff --git a/tests/lean/interactive/t1.lean.expected.out b/tests/lean/interactive/t1.lean.expected.out
index 847e0f943..139da197a 100644
--- a/tests/lean/interactive/t1.lean.expected.out
+++ b/tests/lean/interactive/t1.lean.expected.out
@@ -1,4 +1,3 @@
-Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
 #   Set: pp::colors
   Set: pp::unicode
 Proof state:
diff --git a/tests/lean/interactive/t10.lean.expected.out b/tests/lean/interactive/t10.lean.expected.out
index 846e416ce..fd8276309 100644
--- a/tests/lean/interactive/t10.lean.expected.out
+++ b/tests/lean/interactive/t10.lean.expected.out
@@ -1,4 +1,3 @@
-Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
 #   Set: pp::colors
   Set: pp::unicode
 Proof state:
diff --git a/tests/lean/interactive/t11.lean.expected.out b/tests/lean/interactive/t11.lean.expected.out
index 914f7fed0..bba37b6e0 100644
--- a/tests/lean/interactive/t11.lean.expected.out
+++ b/tests/lean/interactive/t11.lean.expected.out
@@ -1,4 +1,3 @@
-Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
 #   Set: pp::colors
   Set: pp::unicode
 Proof state:
diff --git a/tests/lean/interactive/t12.lean.expected.out b/tests/lean/interactive/t12.lean.expected.out
index 4160901d5..a2f46e3b3 100644
--- a/tests/lean/interactive/t12.lean.expected.out
+++ b/tests/lean/interactive/t12.lean.expected.out
@@ -1,4 +1,3 @@
-Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
 #   Set: pp::colors
   Set: pp::unicode
   Proved: T1
diff --git a/tests/lean/interactive/t13.lean.expected.out b/tests/lean/interactive/t13.lean.expected.out
index e7a96745f..8d1cda17c 100644
--- a/tests/lean/interactive/t13.lean.expected.out
+++ b/tests/lean/interactive/t13.lean.expected.out
@@ -1,4 +1,3 @@
-Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
 #   Set: pp::colors
   Set: pp::unicode
   Proved: T1
diff --git a/tests/lean/interactive/t2.lean.expected.out b/tests/lean/interactive/t2.lean.expected.out
index d7366ef7a..6b29f63b6 100644
--- a/tests/lean/interactive/t2.lean.expected.out
+++ b/tests/lean/interactive/t2.lean.expected.out
@@ -1,4 +1,3 @@
-Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
 #   Set: pp::colors
   Set: pp::unicode
 Proof state:
diff --git a/tests/lean/interactive/t3.lean.expected.out b/tests/lean/interactive/t3.lean.expected.out
index eac4ac983..fb9c744c7 100644
--- a/tests/lean/interactive/t3.lean.expected.out
+++ b/tests/lean/interactive/t3.lean.expected.out
@@ -1,4 +1,3 @@
-Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
 #   Set: pp::colors
   Set: pp::unicode
 Proof state:
diff --git a/tests/lean/interactive/t4.lean.expected.out b/tests/lean/interactive/t4.lean.expected.out
index 3dc9dcba6..2c2853842 100644
--- a/tests/lean/interactive/t4.lean.expected.out
+++ b/tests/lean/interactive/t4.lean.expected.out
@@ -1,4 +1,3 @@
-Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
 #   Set: pp::colors
   Set: pp::unicode
 Error (line: 4, pos: 8) invalid definition, identifier expected
diff --git a/tests/lean/interactive/t5.lean.expected.out b/tests/lean/interactive/t5.lean.expected.out
index d273d31f0..1dd8ef3a0 100644
--- a/tests/lean/interactive/t5.lean.expected.out
+++ b/tests/lean/interactive/t5.lean.expected.out
@@ -1,4 +1,3 @@
-Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
 #   Set: pp::colors
   Set: pp::unicode
   Assumed: magic
diff --git a/tests/lean/interactive/t6.lean.expected.out b/tests/lean/interactive/t6.lean.expected.out
index 8282e464f..f61cedfab 100644
--- a/tests/lean/interactive/t6.lean.expected.out
+++ b/tests/lean/interactive/t6.lean.expected.out
@@ -1,4 +1,3 @@
-Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
 #   Set: pp::colors
   Set: pp::unicode
 Proof state:
diff --git a/tests/lean/interactive/t7.lean.expected.out b/tests/lean/interactive/t7.lean.expected.out
index 0be1633c5..07ceb7bc7 100644
--- a/tests/lean/interactive/t7.lean.expected.out
+++ b/tests/lean/interactive/t7.lean.expected.out
@@ -1,4 +1,3 @@
-Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
 #   Set: pp::colors
   Set: pp::unicode
   Assumed: q
diff --git a/tests/lean/interactive/t8.lean.expected.out b/tests/lean/interactive/t8.lean.expected.out
index 0faa67bd3..a63846fcf 100644
--- a/tests/lean/interactive/t8.lean.expected.out
+++ b/tests/lean/interactive/t8.lean.expected.out
@@ -1,4 +1,3 @@
-Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
 #   Set: pp::colors
   Set: pp::unicode
   Set: tactic::proof_state::goal_names
diff --git a/tests/lean/interactive/t9.lean.expected.out b/tests/lean/interactive/t9.lean.expected.out
index cb593bb07..2a044aefb 100644
--- a/tests/lean/interactive/t9.lean.expected.out
+++ b/tests/lean/interactive/t9.lean.expected.out
@@ -1,4 +1,3 @@
-Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
 #   Set: pp::colors
   Set: pp::unicode
 Proof state:
diff --git a/tests/lean/interactive/test.sh b/tests/lean/interactive/test.sh
index 57fd79098..235acc38a 100755
--- a/tests/lean/interactive/test.sh
+++ b/tests/lean/interactive/test.sh
@@ -13,7 +13,7 @@ fi
 NUM_ERRORS=0
 for f in `ls *.lean`; do
     echo "-- testing $f"
-    cat config.lean $f | $LEAN --lean | tail -n +2 > $f.produced.out
+    cat config.lean $f | $LEAN --lean | tail -n +3 > $f.produced.out
     if test -f $f.expected.out; then
         if diff $f.produced.out $f.expected.out; then
             echo "-- checked"
diff --git a/tests/lean/interactive/test_single.sh b/tests/lean/interactive/test_single.sh
index edd524dc6..7388424ae 100755
--- a/tests/lean/interactive/test_single.sh
+++ b/tests/lean/interactive/test_single.sh
@@ -12,7 +12,7 @@ else
 fi
 f=$2
 echo "-- testing $f"
-cat config.lean $f | $LEAN --lean | tail -n +2 > $f.produced.out
+cat config.lean $f | $LEAN --lean | tail -n +3 > $f.produced.out
 if test -f $f.expected.out; then
     if diff $f.produced.out $f.expected.out; then
         echo "-- checked"