On Wed, 14 Dec 2016, Janus Weil wrote: > 2016-12-14 12:33 GMT+01:00 Jakub Jelinek <ja...@redhat.com>: >> There is gcc.css in the wwwdocs CVS repo. But looking at the wiki pages, >> I see just: > Well, from my side it's not worth to put much effort into this right > now. I have worked around the issues on the mentioned pages in other > ways. > > If the removal of support for HTML tags creates problems on other wiki > pages as well, then one should probably think about adding a > gcc-wiki.css (if possible). Not sure if that's the case.
Let me know when there is anything you'd like to do in that direction, be it adjusting the global gcc.css sheet or introducing gcc-wiki.css, or a combination thereof, Janus. > Btw, https://gcc.gnu.org/wiki/HelpOnThemes mentions a "clever idea to > make CSS wiki editable", which sounds like a useful idea to me (if I > understand it correctly). That also looks like a potential option. Again, happy to help. Gerald