Skip to content

Commit 3d71944

Browse files
committed
fix error test
1 parent a66d357 commit 3d71944

File tree

1 file changed

+2
-11
lines changed

1 file changed

+2
-11
lines changed

test/record_cmd2.expected.out

Lines changed: 2 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -9,12 +9,7 @@
99
"data": "unsolved goals\n⊢ 2 = 2"}],
1010
"env": 0}
1111

12-
{"messages":
13-
[{"severity": "info",
14-
"pos": {"line": 1, "column": 0},
15-
"endPos": {"line": 2, "column": 3},
16-
"data": "Goals accomplished!"}],
17-
"env": 1}
12+
{"env": 1}
1813

1914
{"messages":
2015
[{"severity": "error",
@@ -36,9 +31,5 @@
3631
[{"severity": "info",
3732
"pos": {"line": 3, "column": 0},
3833
"endPos": {"line": 3, "column": 6},
39-
"data": "Try this: exact h2 (h1 p)"},
40-
{"severity": "info",
41-
"pos": {"line": 1, "column": 0},
42-
"endPos": {"line": 3, "column": 6},
43-
"data": "Goals accomplished!"}]}
34+
"data": "Try this: exact h2 (h1 p)"}]}
4435

0 commit comments

Comments
 (0)