I agree that it shoud be installed separately, though of course we want to make it easy for people to try it out. But just running "sage -f git_trac" ought to be easy enough, so lets go with that. And the current branch is not set to build by default anyways.
So as soon as somebody presses the positive review button we can ship it... On Friday, December 27, 2013 1:12:13 AM UTC, R. Andrew Ohana wrote: > > On Wed, Dec 25, 2013 at 12:36 PM, Volker Braun > <vbrau...@gmail.com<javascript:> > > wrote: > > I've been working on a "git trac" subcommand to complement the git suite >> with trac integration instead of the separate UI that the sage -dev scripts >> present. This project is the basis for my release management scripts, so I >> have been eating my own dog food for a while now. I think it is now in a >> state where it would be useful to others, so I propose to integrate it as a >> standard spkg. Obligatory vote: >> >> [ ] Yes, please >> [X ] Make it optional >> [ ] No, you stink >> >> http://trac.sagemath.org/ticket/15587 >> > > IMO, I think for developers who are using git directly that they should be > installing this under /usr/local (or some other prefix that they include in > their paths). In particular, I think it is a very bad idea to integrate the > codebase into the sage codebase for two reasons: > > 1. It will make it more difficult to get to install the tools in > /usr/local (e.g.), as you will have to hunt down in the sage source code to > find the appropriate setup.py. > 2. We will run into the issue of the tools suddenly having a different > feature set while switching between branches (this was incredibly > frustrating for the dev scripts). > > -- > 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+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.
