On Wednesday, March 12, 2014 12:04:54 PM UTC+1, Simon King wrote: > > ... Apparently you need to use git > "the hard way" to let your local branch be pushed to a public branch on > trac, and then you have to manually edit the branch field on trac to > point to the public branch. > > I keep forgetting how to do this. Hence, I'd very much appreciate if > someone > could implement something like > > sage -dev push --ticket=12345 --remote_branch=public/foo/bar > > to push to the specified public branch, and (as a convenience) update > the information on the local branch, such that subsequently > sage -dev push > and > git push > will both push to the previously indicated public trac branch. > > And similarly, if the user has write permission to the branch (e.g., > public branch) attached to a ticket, then > sage -dev push > should push *there* (and not to a new branch u/UserName/...). >
This is now http://trac.sagemath.org/ticket/15943 -- 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/d/optout.
