Oops, sorry again. Missed a part of the discussion here. Me too, I would prefer a more general "Typesetting" section, as suggested in #486144. BR -- Danai