michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean/interactive): remove leftover from test output

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-17 17:29:52 -07:00
parent 05b0f24cb5
commit 1d306c09ee
1 changed files with 0 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/interactive/in1.input.expected.out
View file

@ -1,4 +1,3 @@
DONE
-- BEGININFO
-- SYMBOL|4|22
Type
@ -22,7 +21,6 @@ A
a
-- ACK
-- ENDINFO
DONE
-- BEGININFO
-- SYMBOL|4|22
Type
@ -46,7 +44,6 @@ B
b
-- ACK
-- ENDINFO
DONE
-- BEGININFO
-- SYMBOL|5|22
Type
@ -70,7 +67,6 @@ B
b
-- ACK
-- ENDINFO
DONE
-- BEGININFO
-- SYMBOL|4|22
Type
@ -96,8 +92,6 @@ b
-- ENDINFO
simple.lean:4:0: error: command expected
simple.lean:5:37: error: unknown identifier 'foo'
DONE
DONE
-- BEGININFO
-- SYMBOL|4|22
Type