Docs search not working

Stream: general

[Bolton Bailey]

I have recently noticed that https://leanprover-community.github.io/mathlib4_docs/ and enter a search term, while I will still get a dropdown of query answers, when click the search button, I don't get anything. Has this been changed recently?

[Henrik Böving]

No that's a new one

[Henrik Böving]

looking at the console its most likely caused by eric's escaping changes:
image.png

i'll dig around

[Eric Wieser]

I can take a look too, since I broke it

[Henrik Böving]

Fixed it

[Henrik Böving]

https://github.com/leanprover-community/mathlib4_docs/actions/runs/9555522299 will deploy the fix

[Eric Wieser]

No wonder I had weird merge conflicts