On 2016-11-18 10:05, David Roe wrote: > > > On Fri, Nov 18, 2016 at 3:49 AM, Volker Braun <vbraun.n...@gmail.com > <mailto:vbraun.n...@gmail.com>> wrote: > > The .git dir doesn't have to be in the working tree: > > git --git-dir= --work-tree= > > But I think its very confusing to have another working tree inside the > working tree, thats rather confusing and error prone. E.g. what does "git > commit" do in that situation? IMHO its conceptually much easier to just > do a > separate clone of the repo. And its completely standard git commands. > > > I agree. But I think we should still automate the creation and use of this > separate clone. Where should this clone go? Ask the user when they first > call it? > David
I suggest using "git worktree". This allows to have two working copies sharing the same .git directory and helps with situations like that. Clemens -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To post to this group, send email to sage-devel@googlegroups.com. Visit this group at https://groups.google.com/group/sage-devel. For more options, visit https://groups.google.com/d/optout.
