Skip to content

Put mangle-names in a separate CI target

This reverts the target name change from !266 (merged) that broke the deployment of the documentation.

Merge request reports