There are at least 2 patches where the patchbot currently complains, because it has some problem with ccache:
http://trac.sagemath.org/ticket/14846 and http://trac.sagemath.org/ticket/14347 The shortlog ends as copied below. Does this have consequences for the merging? All the best, Martin git clone . '/tmp/tmpNKZ6HM-sage-git-temp-14347' Cloning into '/tmp/tmpNKZ6HM-sage-git-temp-14347'... done. git branch -f patchbot/base remotes/origin/patchbot/base Branch patchbot/base set up to track remote branch patchbot/base from origin. git branch -f patchbot/ticket_upstream remotes/origin/patchbot/ticket_upstream Branch patchbot/ticket_upstream set up to track remote branch patchbot/ticket_upstream from origin. ./sage -i ccache The Sage installation tree has moved from /tmp/tmpx91IiX-sage-git-temp-14333 to /tmp/tmpNKZ6HM-sage-git-temp-14347 Updating various hardcoded paths... (Please wait at most a few minutes.) DO NOT INTERRUPT THIS. Done updating paths. tee: /tmp/tmpNKZ6HM-sage-git-temp-14347/logs/install.log: No such file or directory Found package ccache in /mnt/storage2TB/patchbot/sage.git/upstream/ccache-3.1.9.spkg Package ccache-3.1.9 is already installed. Use 'sage -f /mnt/storage2TB/patchbot/sage.git/upstream/ccache-3.1.9.spkg' to force a reinstallation. Traceback (most recent call last): File "/mnt/storage2TB/patchbot/sage.git/local/bin/patchbot/patchbot.py", line 453, in test_a_ticket pull_from_trac(self.sage_root, ticket['id'], force=True, use_ccache=self.config['use_ccache']) File "/mnt/storage2TB/patchbot/sage.git/local/bin/patchbot/trac.py", line 316, in pull_from_trac do_or_die("./sage -i ccache") File "/mnt/storage2TB/patchbot/sage.git/local/bin/patchbot/util.py", line 91, in do_or_die raise Exception, "%s %s" % (res, cmd) Exception: 256 ./sage -i ccache 2014-01-06 02:48:46 +0000 11 seconds -- You received this message because you are subscribed to the Google Groups "sage-git" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/groups/opt_out.
