Skip to content

Commit 914077a

Browse files
kim-emkim-em
committed
fix test
1 parent d5bdad8 commit 914077a

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

‎tests/lean/run/grind_question_mark_suggestions.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
import Lean
22

3-
set_premise_selector Lean.LibrarySuggestions.sineQuaNonSelector
3+
set_library_suggestions Lean.LibrarySuggestions.sineQuaNonSelector
44

55
-- Test that grind? +suggestions does NOT include +suggestions in its output
66
/--

0 commit comments

Comments
 (0)