rolfmorel wrote: I am happy for the PR to be merged. As such, I have squashed the documentation fix-up commit. If somebody, e.g. @banach-space or @rengolin, could help with merging, that would be much appreciated! https://github.com/llvm/llvm-project/pull/101561