Hello, ok, I guess this is the source of the problem. Could you
1) copy again your original sage dir into a new dir 2) type ./sage inside this new dir maybe it will take care of the change of dir ? I am not sure.. Could some readers of the devel-group help us here ? How to safely duplicate a sage-installation ? Frederic Le samedi 18 avril 2015 20:31:16 UTC+2, Martin R a écrit : > > > Am Samstag, 18. April 2015 20:11:12 UTC+2 schrieb Frédéric Chapoton: > > Hello, > > > Do you confirm that the branch patchbot/ticket_merged > > is the same as 6.7.beta1 ? > > you can check that using > > "git log " > > the top line should have the tag 6.7.beta1. > > > If so the failure has probably nothing to do with the patchbot, but > means that your sage is somewhat broken. It would probably take somebody > else to help you find out why.. > > Looks like it, see below... > > > How did you get your sage? by cloning from git? > > Yes, but: I cloned it quite a while ago (I guess its sage 6.5), and was > mainly working on the findstat ticket. I was pointed to the patchbot by > the blue blob on the ticket and wanted to find out more. > > So I copied the whole directory to a new one, ran make and then sage -i > patchbot. I guess copying the directory to get a second sage is probably > not the right thing to do. What should I do? Compiling sage takes hours > :-( > > Martin > > commit 9d18e27362ed6c6ca896e6731023d1f4b954b7af > Author: ... > Date: Wed Apr 15 23:14:05 2015 +0200 > > Updated Sage version to 6.7.beta1 > > commit 2857ebf20bfdd2c22cb8f08bb1e281543232ed42 > Merge: f4ee46d 42e505e > Author: Release Manager <XXX@XXX> > Date: Wed Apr 15 21:46:47 2015 +0200 > > Trac #18205: mistune buggers up sage install > > -- 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 [email protected]. To post to this group, send email to [email protected]. Visit this group at http://groups.google.com/group/sage-devel. For more options, visit https://groups.google.com/d/optout.
