Doc: workaround to avoid that doxygen interprets /* in pages.

This problem apparently appeared with recent versions of Doxygen because
it used to work before.