GitHub Community
https://github.com/FStarLang/FStar/wiki search is only getting page titles #143677
Unanswered
briangmilnes
asked this question in
Repositories
https://github.com/FStarLang/FStar/wiki search is only getting page titles
#143677
Replies: 1 comment
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
Select Topic Area
Question
Body
I can't find documentation on how to configure wiki search to search inside the pages.
Anyone know how to set this up?
Beta Was this translation helpful? Give feedback.
All reactions