mirrors/jj
1
0
Fork 1
mirror of https://github.com/martinvonz/jj.git synced 2024-10-24 07:32:54 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions 6

merge_view: remove heads removed by other side also in Google repos

Browse source 
When I addded the workaround in 256988de65, I missed the comment
just below explaining that heads removed by the other side were
already handled. Since that's not handled when using non-default
indexes now, we need to handle it in an `else` block.
This commit is contained in:
Martin von Zweigbergk 2024-05-15 17:16:31 -07:00 committed by Martin von Zweigbergk
parent 0a39cfdbe2
commit 66aced5dc8
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
lib/src/repo.rs
View file

@ -1629,9 +1629,13 @@ impl MutableRepo {
if self.index.as_any().is::<DefaultMutableIndex>() { if self.index.as_any().is::<DefaultMutableIndex>() {
self.record_rewrites(&base_heads, &own_heads); self.record_rewrites(&base_heads, &own_heads);
self.record_rewrites(&base_heads, &other_heads); self.record_rewrites(&base_heads, &other_heads);
// No need to remove heads removed by `other` because we already
// marked them abandoned or rewritten.
} else {
for removed_head in base.heads().difference(other.heads()) {
self.view_mut().remove_head(removed_head);
}
} }
// No need to remove heads removed by `other` because we already marked them
// abandoned or rewritten.
for added_head in other.heads().difference(base.heads()) { for added_head in other.heads().difference(base.heads()) {
self.view_mut().add_head(added_head); self.view_mut().add_head(added_head);
} }