Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We鈥檒l occasionally send you account related emails.

Already on GitHub? Sign in to your account

Suggestion: introducing fuzzy-search *OR* adding links to the footer 馃攳馃搩馃Χ馃徏 #139

Open
thierrymarianne opened this issue Aug 25, 2022 · 0 comments
Assignees
Labels
enhancement New feature or request

Comments

@thierrymarianne
Copy link

thierrymarianne commented Aug 25, 2022

Hello 馃憢馃徏,

Context

First of all, thank you for organizing the yesterday's Z3 workshop!
It was amazing and I've learnt a lot.

Issue

I was looking for some reference documentation,
just before noticing the guide doesn't have a search engine
(I might have missed it though 馃槄).

Is that something which could be "fixed" somehow maybe?

As I understood, since the guide is fully running on the client side,
I was wondering if there would not be an existing fuzzy-search option
offered by facebook/docusaurus

Discussion

I found out from docusaurus documentation that local search might be a viable option

local search use suggested by docusaurus documentation as highlighted

Perhaps, some of you may have some thoughts to share on this usability topic?

Mitigation

In order to mitigate the originally encountered issue,
Links to both API reference and parameters could be added to the footer.

@thierrymarianne thierrymarianne changed the title About searching the Z3 guide Suggestion: Allowing to fuzzy-search the Z3 guide Aug 25, 2022
@thierrymarianne thierrymarianne changed the title Suggestion: Allowing to fuzzy-search the Z3 guide Suggestion: introducing fuzzy-search form in the menu Aug 25, 2022
@pelikhan pelikhan added the enhancement New feature or request label Aug 25, 2022
@thierrymarianne thierrymarianne changed the title Suggestion: introducing fuzzy-search form in the menu Suggestion: introducing fuzzy-search 馃攳馃搩 Aug 25, 2022
@thierrymarianne thierrymarianne changed the title Suggestion: introducing fuzzy-search 馃攳馃搩 Suggestion: introducing fuzzy-search *OR* adding links to the footer 馃攳馃搩 Aug 25, 2022
@thierrymarianne thierrymarianne changed the title Suggestion: introducing fuzzy-search *OR* adding links to the footer 馃攳馃搩 Suggestion: introducing fuzzy-search *OR* adding links to the footer 馃攳馃搩馃Χ馃徏 Aug 25, 2022
@rlisahuang rlisahuang assigned pelikhan and unassigned rlisahuang Aug 30, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

3 participants