Skip to content

Conversation

@KyleHerndon
Copy link
Contributor

Duplicate of #2526
I made a bad rebase/push and accidentally closed the old PR

@KyleHerndon KyleHerndon requested a review from sogartar October 27, 2025 21:24
@github-actions
Copy link
Contributor

github-actions bot commented Oct 27, 2025

Coverage report

Click to see where and how coverage changed

FileStatementsMissingCoverageCoverage
(new stmts)
Lines missing
  sharktank/sharktank/types
  module.py 7-31, 35
  sharktank/sharktank/utils
  iree.py 130, 286
  sharktank/tests/utils
  iree_test.py
Project Total  

This report was generated by python-coverage-comment-action

@sogartar
Copy link
Contributor

Duplicate of #2526
I made a bad rebase/push and accidentally closed the old PR

You can force-push to overwrite the commit history.

git push -f origin users/kyle/modulify

I think you can reopen your previous PR, but you would need to close this PR first as they have the same PR branch name.

@KyleHerndon
Copy link
Contributor Author

git push -f origin users/kyle/modulify

I tried this. As far as I could tell, as soon as a branch has zero commits on it (I accidentally had my HEAD on main when I pushed), you can no longer reopen the PR. After force pushing the branch again continued to show 0 commits on the PR.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants