On Sat, Dec 9, 2017 at 1:27 PM, Volker Braun <vbraun.n...@gmail.com> wrote: > The easy solution: Just wait for the next beta > > If you absolutely positively can't wait you can get the current branch from > my github page; If you merge with that you'll find the conflict. But don't > ever publish that merge as it is bound to be rewritten before the next beta > is released.
Instead of using a branch on your personal github fork, why don't we use a branch on the main git.sagemath.org repository for this purpose, that's easier to find? I'm not saying it should be the "master" branch since it gets overwritten regularly if/when it needs to be backtracked, but IMO your merge branch is much closer to anything Sage has resembling a dev head. Best, Erik > On Saturday, December 9, 2017 at 7:54:48 AM UTC+1, Ralf Stephan wrote: >> >> Hi, >> A positive-review ticket was sent back because of merge conflict. >> Somewhere there has to be the info which other ticket caused it so I can >> provide a conflict fix. I also remember Volker giving me a web address once >> in such a case but it's buried in a ticket. >> >> So, I want to put a howto in a Wiki page that explains where to look and >> what to do. >> >> Can you help please? >> > -- > 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. -- 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.
