Zulip Chat Archive
Stream: general
Topic: Duckduckability of documentation
Gabriel Ebner (Jul 08 2020 at 08:02):
Motivated by @Jasmin Blanchette's rant on the other thread, I tried googling for pp_nodot. To my surprise, it didn't find anything official:
- It should find this Zulip archive page: https://leanprover-community.github.io/archive/stream/113488-general/topic/Lean.203.2E16.2E0.html
- And maybe this PR: https://github.com/leanprover-community/lean/pull/297
But neither duckduckgo nor google nor bing find these:
- https://duckduckgo.com/?q=%22pp_nodot%22
- https://www.google.com/search?q=%22pp_nodot%22
- https://www.bing.com/search?q=%22pp_nodot%22
Resident computer expert and SEO guru @Rob Lewis, do you have any ideas?
Rob Lewis (Jul 08 2020 at 08:33):
The Zulip archive doesn't generate a sitemap iirc. This would probably help a little. It definitely gets crawled anyway, and Google directs traffic there, but not as much as you'd hope.
Rob Lewis (Jul 08 2020 at 08:33):
Why it misses the PR, I have no idea. I've always thought Google was pretty good about directing to Github issues/PRs.
Rob Lewis (Jul 08 2020 at 08:34):
Maybe it's because pp_nodot only appears in <code> on the page? This is a random guess.
Last updated: Dec 20 2023 at 11:08 UTC