Skip to content

Commit 9239132

Browse files
KhaKha
committed
revert test change
1 parent 3ae3241 commit 9239132

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

‎tests/lean/interactive/unknownIdentifierCodeActions.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ module
33

44
public section
55

6-
#check Lean.Server.Test.Refs.Test1
6+
#check Lean.Server.Test.Refs.test1
77
--^ codeAction
88

99
example : LeanServerTestRefsTest0

0 commit comments

Comments
 (0)