On Wed, 30 Oct 2024 at 03:46, Daniel Gustafsson <daniel@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
