I’ll see if we can make HTML cleaner/simpler so that it can work with PDF, or alternatively, we could ignore the entire section in the PDF…

Right. Would be nice to have this in the PDF, but if we can’t it’s no big deal. I doubt many people actually use the PDF.