[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/
js-margin.patch
Description: Text Data
| [Prev in Thread] |
Current Thread |
[Next in Thread] |
- js-info patch for margin spacing,
Per Bothner <=