Join GitHub today
GitHub is home to over 31 million developers working together to host and review code, manage projects, and build software together.Sign up
doc: update AUTHORS list #26383
I wanted to apologise for that, that comment deletion was not intentional, and I just recently noticed it.
I don't remember deleting a comment here (on a purpose or not), it must have been accidental, most likely while I was commenting on this issue from my phone.
Unfortunately, I do not have the means of restoring a deleted comment or checking what exactly was in that comment (GitHub does not provide that afaik). The only way that I know how it could be restored is if you re-post it from your side.
I really hope that nothing was missed, but in any case — please feel free to restore that comment if you want to.
this is what I have in mailbox matching to that day and time - the accidentally deleted comment, for the record: