git: refresh the index after resetting it

Closes #3786.
This commit is contained in:
Martin von Zweigbergk 2024-05-29 21:22:32 -07:00
parent 3090adfd5c
commit 2834b37888
No known key found for this signature in database

View file

@ -969,6 +969,8 @@ pub fn reset_head(
};
if !skip_reset {
git_repo.reset(new_git_commit.as_object(), git2::ResetType::Mixed, None)?;
// Refresh the index since some scripts expect that.
git_repo.index()?.update_all(["."], None)?;
}
} else {
// Can't detach HEAD without a commit. Use placeholder ref to nullify the HEAD.