[Dune] Doxygen page names

[Christian Engwer]

Hi Timo,

> Is there some option to doxygen I’m missing? Or some magic in Dune that I’m missing?
> It would be nice if someone could point me to the mechanism behind.

There is a flag in the doxygen configuration...

> # If the SHORT_NAMES tag is set to YES, doxygen will generate much shorter
> # (but less readable) file names. This can be useful if your file systems
> # doesn't support long names like on DOS, Mac, or CD-ROM.
> SHORT_NAMES            = YES

Sadly this is necessary for building tarballs, the mangled file names will otherwise become too long.

On the website this does not happen, as the website is not using the Doxystyle from dune-common.

Ciao
Christian