Hello Peter,
> I think the fix belongs into the web site CSS, so there is nothing to
> commit into PostgreSQL here.
Indeed, the changes were only for the "remove nesting" solution.
> I will close the commit fest entry, but I have added a section to the
> open items list so we keep track of it.
> (https://wiki.postgresql.org/wiki/PostgreSQL_10_Open_Items#Documentation_tool_chain)
I put forward that the quick workaround a colleague of mine suggested (aka
something like code code { font-size: 100%; important! }) could also be
applied to the web site CSS while waiting for a more definite answer which
might take some pretty unknown time close to never?
--
Fabien.