Ping. Patch still applies.
On Fri, May 10, 2024 at 03:16:18PM +0200, Christoph Heiss wrote:
> Works the same as in our PBS documentation and is generally common for
> documentations.
>
> Very useful for linking specific sections of the documentation in other
> places. Previously, this always had t
On Fri May 10, 2024 at 3:16 PM CEST, Christoph Heiss wrote:
> Works the same as in our PBS documentation and is generally common for
> documentations.
>
> Very useful for linking specific sections of the documentation in other
> places. Previously, this always had to be done by getting the correct
