Skip to content

Commit 01d6752

Browse files
committed
remove unnecessary tests
1 parent 1af9f40 commit 01d6752

File tree

2 files changed

+0
-25
lines changed

2 files changed

+0
-25
lines changed

tests/lean/interactive/namespaceCompletion.lean

Lines changed: 0 additions & 12 deletions
This file was deleted.

tests/lean/interactive/namespaceCompletion.lean.expected.out

Lines changed: 0 additions & 13 deletions
This file was deleted.

0 commit comments

Comments
 (0)