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
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
anchor from the HTML directly via e.g. browser devtools.
Signed-off-
