Feature request: search box in the archive.

Stream: new members

[Manoj Kummini]

Is it possible to add a search box to <https://leanprover-community.github.io/archive/>? One could use the inurl: directive in google but having to type it each time is a minor inconvenience.

[Bryan Gin-ge Chen]

Our Zulip archive is generated by the scripts here. I don't know that @Rob Lewis will have time to work on it anytime soon, but I think PRs are welcome!

[Eric Wieser]

Is there much point? The search inside zulip is almost certainly more powerful

[Bryan Gin-ge Chen]

Well, I could imagine people not wanting to sign into Zulip.

[Manoj Kummini]

Bryan Gin-ge Chen said:

Well, I could imagine people not wanting to sign into Zulip.

That was the reason, mostly.

[Patrick Massot]

I'm not sure we want to invest too much time in this archive. The main point is that search engines can index it so that people can discover that we have good stuff here and sign in. But I think there is no much point into encouraging people not to come here.