-

[riveronly]

[KevinnZou]

@riveronly Thanks for your contribution. I am currently traveling and will begin reviewing this PR next week. Thank you again!

[KevinnZou]

@msasikanth Could you also have a review on this PR? Thanks!

[riveronly]

@KevinnZou please delete this PR and I will resubmit it

[riveronly]

@KevinnZou I accidentally used the wrong email address to submit. Can you submit a work order to github to delete this mr? This is very important to me, thank you.

[msasikanth]

@KevinnZou I accidentally used the wrong email address to submit. Can you submit a work order to github to delete this mr? This is very important to me, thank you.

I don't think there is a way to delete the PR on GitHub. The only option is to close it and open a new one, if it has to be deleted it needs to be from GitHub support (which I don't think will happen in most scenarios).

[msasikanth]

fwiw I see only the last commit in this PR has a different username. So, you can just drop that commit and force push to your repo. That should clear it.

[riveronly]

Removing commit and force push will change the header information and it will not be the same merge request. Merge request records can be deleted only if github supports it. But there is no other way to delete this commit.

[KevinnZou]

@riveronly I found that you already submitted a new PR. We can directly review that one and dismiss this one.