doc-gen icon indicating copy to clipboard operation
doc-gen copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Add opensearch support

Open eric-wieser opened this issue 2 years ago • 7 comments

eric-wieser avatar Mar 03 '22 18:03 eric-wieser

#deploy

eric-wieser avatar Mar 03 '22 18:03 eric-wieser

This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!

github-actions[bot] avatar Mar 03 '22 18:03 github-actions[bot]

This seems not to work

eric-wieser avatar Mar 16 '22 14:03 eric-wieser

Any idea what went wrong?

#deploy

gebner avatar Mar 16 '22 14:03 gebner

I think Google only respects the meta tag if it finds it on the homepage at the root of the URL

eric-wieser avatar Mar 16 '22 14:03 eric-wieser

This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!

github-actions[bot] avatar Mar 16 '22 15:03 github-actions[bot]

Yeah, I can add it in firefox but not in chromium.

And searching with spaces is not supported: https://leanprover-community.github.io/mathlib_docs_demo/find/nat+cast

gebner avatar Mar 16 '22 15:03 gebner