Note the big red warning on the top of the page. Use public/sage-git/master instead of master until things settle down.
git fetch trac u/user/description git checkout -b trac_master FETCH_HEAD make On Thursday, September 19, 2013 1:20:14 PM UTC+1, martin....@gmx.net wrote: > > I'm still trying to come to grips with the transition to git. I hear about > it in this > thread<https://groups.google.com/forum/#!topic/sage-devel/ZX_k2USc7bI>and now > wanted to use it for a > requested rebase <http://trac.sagemath.org/ticket/13608#comment:22>. Here > is what I did: > > 1. Checked out sage git repository from ssh:// > g...@trac.sagemath.org:2222/sage.git as outlined > here<http://sagemath.github.io/git-developer-guide/manual_git.html#the-trac-server> > . > 2. Tried “make”, received complaint about missing spkg directory. > 3. Extracted spkg directory from sage 5.11 source tarball. > 4. “make” succeeded, but apparently used the tarball sources for core > parts of sage as well. > 5. symlinked “src” to “devel/sage-dev” and did “./sage -b dev”, got a > version which uses my sources. > 6. Used git to branch, then rebased my patch to that. > 7. “git status” now mentions a large number of untracked things, among > them src/sage/**/*.c, src/c_lib/src/*.os and so on. > > Is the above a reasonable approach to do git-based sage development at the > current moment? > Is there a better way, and if so, where is it documented? > Can I reasonably use the above to submit a branch for patchbot, or would > you expect things to break due to the way I set things up? > Will .gitignore settings take care of all these untracked generated files > one day? Is there any ticket keeping track of this? > > -- 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.
