Kai Uwe Broulik authored Nov 12, 2022 and Volker Krause committed Nov 13, 2022

There's not really any need for elaborate HTML styling as provided
by RichText.

More importantly, though, this lets us easily (without adding
custom CSS) set linkColor to the text color. Currently, links use
the default blue color which can clash with the background quite harsh.

Since links are underlined, they are still marked.