On Fri, Nov 18, 2016 at 2:45 AM, Volker Braun <vbraun.n...@gmail.com> wrote:
> On Friday, November 18, 2016 at 8:12:32 AM UTC+1, David Roe wrote: >> >> Create a new git trac subcommand to replace `git trac checkout 1234`, say >> `git trac old 1234`. This would fetch the branch, check it out into a >> completely separate folder within ($SAGE_ROOT/merge_tree or something), >> merge in develop. If the merge is successful, create a new branch and pull >> the changes in. This ends up with only a few files changing if you started >> at develop. If the merge is not successful, report to the user and ask >> them to fix the merge in >> $SAGE_ROOT/merge_tree. There would then be some way to resume and pull >> in the changes. >> >> There are some details to fill in, but I think that an approach like this >> can work. It does mean having another 100MB working tree floating around >> just for merging into, and also stepping a bit further away from normal git >> practices. >> >> Any other ideas? >> > > I'd just clone the repo to a separate directory, nothing except the > standard git commands necessary. > Yeah, just cloning is probably better. I was thinking for a bit that we could avoid the duplicated space of having a separate .git folder, but I don't think it's worth the added complications. Certainly, the ideal solution is to fix Cython so that the timestamp changes don't cause trouble, either by fixing the problems with cycache or by using hashes as William suggests. But that's not going to happen quickly, and I'd like to have a workaround. A new git trac command is opt-in and fairly easy to implement. Volker, does this sound like a reasonable pull request for git-trac-command? David -- 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.
