Need to amend the name of the GitHub docu bot

Question

Closed this issue 3 years ago · 1 comments

Answer 1 · 2021-07-28T12:50:32.000Z

Done, with the help of @Shegox (who has access) (thanks!)