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. -- Sent via pgsql-hackers mailing list (pgsql-hackers@postgresql.org) To make changes to your subscription: http://www.postgresql.org/mailpref/pgsql-hackers
