On Wed, 30 Oct 2024 at 03:46, Daniel Gustafsson <dan...@yesql.se> wrote: > On the whole I wonder if we shouldn't just go with the proposal since it > improves the status quo, optimizing for users who hover to get link anchors on > mobile probably isn't worth the investment in time.
My primary motivation for hacking on this was to try to reduce the confusion and reports about the mysterious #. I imagine the patch will improve that situation, but it does risk us getting new reports if there's something off with these changes. My thoughts are that it doesn't seem excessively critical that this is perfect on the first attempt. I'd be happy to see us try to improve this. Maybe if there's some better way, someone will appear and tell us how to do it properly. I am hopeful that we're not just swapping one problem for another. Do you have access to make this change? I think it needs to go into https://www.postgresql.org/media/css/main.css David
