bad merge

Apparently the additions introduced through !347 (merged) which are reported to have been "merged" do not yet seem to have arrived at our official compendium. This is relevant, because the lack of up to date documentation there has lead to additional work as documented with Ticket:2021111541013107 (in OTRS).

What is the recommended course of action here?

(I assigned @michmuel--tu-dresden.de to this, because I once heard that he does merges)

added CI/CD Pipeline label

assigned to @michmuel--tu-dresden.de

changed the description

mentioned in merge request !412 (merged)

Will be fixed with !412 (merged).

New #221 (closed) for fixing auto merge.

closed