On 4/12/17 09:50, Bruce Momjian wrote:
> On Wed, Apr 12, 2017 at 01:31:51PM +0200, Magnus Hagander wrote:
>> I think that only leaves the change to the javascript code that Bruce sent.
>> Let's see if we can figure out a way to do that one without requiring
>> javascript, but after that we have covered all listed issues I think?
>
> Well, we have been using JavaScript for years, so my patch only fixes
> the JavaScript we already have. Seems applying the fix now makes sense
> and then we can ponder other methods.
I have googled a bit. These two articles describe what I think is the
issue we are trying to address:
http://code.stephenmorley.org/html-and-css/fixing-browsers-broken-monospace-font-handling/
http://meyerweb.com/eric/thoughts/2010/02/12/fixed-monospace-sizing/
The recipe in the first one seems to work somewhat, but not quite as
well as the current javascript. (The recipe in the second article is
ultimately equivalent but more verbose.)
I tend to agree with Bruce that we could just fix this within the
current framework. But if we want to make a change, there is the
information.
--
Peter Eisentraut http://www.2ndQuadrant.com/
PostgreSQL Development, 24x7 Support, Remote DBA, Training & Services
