Zulip Chat Archive

Stream: general

Topic: git branch

Patrick Massot (Apr 20 2018 at 08:12):

@Simon Hudon you got your git branches mixed up. Your two PR https://github.com/leanprover/mathlib/pull/109 and https://github.com/leanprover/mathlib/pull/104 are currently mixed up

Kevin Buzzard (Apr 20 2018 at 08:12):

it's all or nothing :-)

Simon Hudon (Apr 20 2018 at 11:29):

That's all they get you! If you want the fix to wlog, you need to pay for ext ;-)

Last updated: Dec 20 2023 at 11:08 UTC