Skip to content

Commit 9c594e3

Browse files
committed
cleanup
1 parent cabbe08 commit 9c594e3

File tree

1 file changed

+1
-5
lines changed

1 file changed

+1
-5
lines changed

test/pickle_scoped_notation.in

+1-5
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,5 @@
1212

1313
{"cmd": "example : 39 = 2 ! := rfl", "env": 5}
1414

15-
{"cmd": "open Lean.Compiler", "env": 5}
16-
17-
{"cmd": "unsafe example : ◾ := sorry", "env": 7}
18-
19-
{"pickleTo": "test/f.olean", "env": 7}
15+
{"pickleTo": "test/f.olean", "env": 5}
2016

0 commit comments

Comments
 (0)