Zulip Chat Archive

Stream: new members

Topic: Waiting for merge


view this post on Zulip Ashwin Iyengar (Mar 10 2021 at 15:40):

If I have a branch which is waiting to be merged, and then I want to keep writing code on top of that branch, is there a way using leanproject to start a new branch from that previous branch? Or do I use git branch?

view this post on Zulip Johan Commelin (Mar 10 2021 at 15:41):

You have to use git (as far as I know)

view this post on Zulip Johan Commelin (Mar 10 2021 at 15:41):

But it still makes sense to checkout the old branch and run leanproject get-cache there, before you switch to the new branch.

view this post on Zulip Yakov Pechersky (Mar 10 2021 at 15:42):

git checkout origin/my-pushed-branch
git checkout -b my-derivative-branch

view this post on Zulip Ashwin Iyengar (Mar 10 2021 at 15:43):

Great thanks.


Last updated: May 11 2021 at 23:11 UTC