On 4/17/20 8:51 PM, Tom Lane wrote:
> "Jonathan S. Katz" <jkatz@postgresql.org> writes:
>> Seems reasonable. Is the change committed yet so I can test against it?
>
> Just pushed it a moment ago.
Thanks!
I went ahead and tweaked it a bit (attached) to give a little bit of
space between the lead line + the table edge (example screenshot
attached). I've attached the update patch. I tested in Chrome, FF,
Safari, and varied my window size.
I then started testing on my phone, and noticed that the font is smaller
in the tables than elsewhere. I believe this was done initially at first
to manage the old table design, so perhaps this is an opportunity to
bump the font up on it.
Thoughts?
Jonathan
