If you have pushed it then it is on our git server. You can just manually add a comment "I pushed branch X to git" until this is fixed.
On Saturday, December 21, 2013 11:12:38 AM UTC, John Cremona wrote: > > On 21 December 2013 08:22, R. Andrew Ohana <andrew...@gmail.com<javascript:>> > wrote: > > Ok, the issue should hopefully be fixed now. > > > > > > On Fri, Dec 20, 2013 at 7:41 AM, John Cremona > > <john.c...@gmail.com<javascript:>> > > > wrote: > >> > >> I have a variation: I successfully pushed a new commit to #15554, then > >> went onto trac to enter the commit hash manually, but get the error > >> message > > > > > > Although in your case, you haven't actually pushed to the branch yet. > I've > > added a nop (instead of error) if the commit field is invalid (this > should > > only happen if someone enters the commit field manually -- which no one > > should ever have to do). > > Please tell me what to do -- checkout that branch again locally and do > another sage- dev push? > > John > > > > > -- > > Andrew > > > > -- > > 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+...@googlegroups.com <javascript:>. > > To post to this group, send email to > > sage-...@googlegroups.com<javascript:>. > > > Visit this group at http://groups.google.com/group/sage-devel. > > For more options, visit https://groups.google.com/groups/opt_out. > -- 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 http://groups.google.com/group/sage-devel. For more options, visit https://groups.google.com/groups/opt_out.
