Pipeline #15368 passed
Pipeline passed for 8fb0529f on fix-copy-n-paste-bug 6 years ago
Pipeline #16553 passed
Pipeline passed for 6e567183 on master 6 years ago
@markus.blatt , is this okay?
merged
mentioned in commit 6e567183