Skip to content

Commit 40d3af5

Browse files
kim-emkim-em
committed
Merge branch 'library_suggestions' into suggestion_combinators
2 parents 3bd8dee + 914077a commit 40d3af5

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)