Thank you for this info. I'll submit my patch to archweb first.
On Sat, Jun 9, 2018 at 10:30 AM, Lukas Fleischer <[email protected]> wrote: > On Fri, 08 Jun 2018 at 23:04:20, nodivbyzero wrote: >> --- >> web/html/css/archweb.css | 12 ++++++++++-- >> 1 file changed, 10 insertions(+), 2 deletions(-) >> [...] > > We keep this in sync with the actual archweb CSS. So instead of doing > this, we should copy and commit the most recent version from archweb.
