breaking builds with unrelated commit

Stream: general

[Yakov Pechersky]

How does the difference between 72d0f8c (working) and 8dd5420 (broken) break the test/norm_fin.lean file??!!

[Yakov Pechersky]

I think I see, it's just a large breaking commit.

[Bryan Gin-ge Chen]

It looks like 8dd5420 is not in the same branch as 72d0f8c, the merge commit between those branches is d22811e which comes later.

edit: linked the wrong commit.

[Yakov Pechersky]

Thanks, that helps clear that up.

[Bryan Gin-ge Chen]

I managed to coax git to print a nice graph of the various branches there, see gist.