bug-texinfo
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

js-info patch for margin spacing


From: Per Bothner
Subject: js-info patch for margin spacing
Date: Fri, 12 Feb 2021 21:36:45 -0800
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.7.0

This patch to the js-info reader deals with some unequal margin
spacing surrounding the initial page vs other pages.

This is discussed here, including a proposed patch from Gavin:
https://lists.gnu.org/archive/html/bug-texinfo/2020-08/msg00024.html

Unfortunately, I couldn't get Gavin's patch to work reliably.
One problem is avoiding unneded horizontal scrolling, which
can be fixed with the 'box-sizing' property.

In any case, it doesn't follow that the default browser
margin spacing for <body> should also be used main page display
area - it should probably be a separately tweakable setting.
My patch has 1.5em left padding and 0.5em right padding,
with reduced left padding (0.5em) for the navigation bar.

I've mostly tested this with the "html structure revisited"
patch from my previous message.
--
        --Per Bothner
per@bothner.com   http://per.bothner.com/

Attachment: js-margin.patch
Description: Text Data


reply via email to

[Prev in Thread] Current Thread [Next in Thread]