On Thu, Jan 08, 2026 at 11:40:16AM +0100, Thérèse Godefroy wrote: > Hi Bruno, all, > > > A year ago, you were working on GNU's /style.css. [1] > > So I guess you are the best person to evaluate the 4 problem reports > > from Gavin Smith in > > https://lists.gnu.org/archive/html/bug-gnulib/2026-01/msg00015.html > > https://lists.gnu.org/archive/html/bug-gnulib/2026-01/msg00016.html > > ? > > > * @group creates a thin blank line on the coloured background in @example. > > > This is due to a margin on the div.group element. > > > > > > This appears to be set in a rule in the included file > > > https://www.gnu.org/style.css: > > > > > > /* For make, gawk, bison, etc. */ > > > div[class*="example"] > pre + pre, div[class*="example"] > .group { > > > margin: 3px 0; > > > } > > > > > > The @group command is for affecting page breaks, which make no sense > > > in an HTML file, and so @group should have no user-visible effect in HTML. > > > > > @group is converted to <div class="group">. That's why I thought it > could be styled. The idea was to separate groups of commands for > clarity. > I removed this style. > > If you don't want this texinfo command to affect HTML, you might > consider suppressing its conversion.
It should not affect HTML as traditionally read in a browser, with everything on a page. But in other contexts, for example for an EPUB reader where HTML is presented like a book, it could be relevant to keep the information that there was a @group and use it in some way to avoid a page break. I have no idea if this is actually doable nor how, but at least in principle it could be useful. Also, even though it is not what is described in the documentation, nor how @group is used in general, we could imagine that in some cases, the @group block could have a more semantic use, in which case having the kind of CSS rules you proposed could be relevant. -- Pat
