On Fri, Dec 11, 2020 at 8:14 PM <dieter@REDACTED> wrote: > First I am asking: > - do you think it is worth the effort? Yes. > - is it sufficient to patch the xml files? Yes. > If yes, I think that a pull request on github would be the method of choice, right? Yes. /Björn -- Björn Gustavsson, Erlang/OTP, Ericsson AB