Skip to content

Commit e5e0dce

Browse files
robsimmonsrobsimmons
committed
Move test file
1 parent eddd72c commit e5e0dce

File tree

1 file changed

+0
-0
lines changed

1 file changed

+0
-0
lines changed

tests/lean/run/identifierSuggestions.lean renamed to tests/lean/run/idSuggestStandalone.lean

File renamed without changes.

0 commit comments

Comments
 (0)