[Maxima-discuss] CSS for textbox, titlebox, and synopsisbox?

[Raymond T. <toy...@gm...>]

I'm in the process of trying to clean up the CSS for the manual by using 
variables to make it easier to set colors for light and dark mode. This 
is fairly straightforward, but I noticed that there is CSS for 
|div.textbox|, |div.titlebox|, and |div.synposisbox|.

A quick grep of the HTML files shows that there is no occurrence of 
"textbox", "titlebox", or "synposisbox" anywhere.

Does anyone know what these are for? Is it safe to delete these?

​