Open jjasghar opened 1 week ago
To wipe out the files in the PR, we need to force push to the submitter's fork while the PR is still open. A maintainer should have this permission.
First, in your local clone, checkout the PR using the gh
command. Using the gh
command sets the proper config for pushing back to the submitter's fork.
gh pr checkout pr_number
where pr_number
is replaced by the PR number.
The you need to remove all the troublesome commits.
git reset --hard HEAD^
removes one commit. Repeat as necessary to remove all desired commits.
Then we need to push back to the submitter's fork. If the submitter used a branch (other than main
):
git push --force
If however the submitter made the PR from their main
branch:
git push git@github.com:github_user/taxonomy.git HEAD:main --force
where github_user/taxonomy
is replaced by the submitter's fork.
After this, the PR can be otherwise changed (edit comments, close).
See https://github.com/instructlab/dev-docs/issues/24 which covers this same topic.
We should create a standard process for possible leaked or unapproved knowledge submissions.
Something along the lines of: