On 2014-12-26, Nathann Cohen <nathann.co...@gmail.com> wrote: > --f46d043c7edc287181050b1f0d5c > Content-Type: text/plain; charset=UTF-8 > > Helloooooooooo everybody ! > > There is no pub in a radius of 40km of where I live, so I spend my evenings > rewriting Sage's developer manual. > > Tonight I have two questions for you: > > 1) should we keep the "Sage dev" scripts in Sage ? > 2) Should we keep it in the doc ? > > http://www.sagemath.org/doc/developer/ > > Several reasons: > - Most of our developer's manual is about 'how to use git'. We have: > - First Steps with Git > - Git and Trac Integration (contains 'git-trac' and the dev scripts) > - Git tips and tricks (contains 'git the hard way') > (All of which appears before the 'sage-specific' doc. Perhaps we should > reverse that) > > - The 'dev scripts' page begins with a 'hint' recommending to NOT use them > (feels like a deprecation already) > > - A tool that we do not use ourselves will not be debugged either > > Given that we have been using Git for a while now, perhaps we can more > easily make up our minds on this respect ? > > I believe that two ways to contribute (regular git + git trac) is already a > lot, and that we should stick to that. It may also be slightly clearer to > newcomers who wonder which of the 3 (!!!) different ways to contribute they > should pick. > > What do you think ?
IMHO dev scripts should be retired. Does anyone use them? By the way, I noticed some change in the behaviour of trac git server; it seems that fetching u/foo/bar automatically results in creation of a local branch trac/u/foo/bar. Is this documented anywhere? Cheers, Dima > > Good evening, > > Nathann > -- 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.
