Closed rwst closed 10 years ago
This would make trivial patches much more expensive--is make not correct for the docs?
Leftover files from previous runs are not deleted by git checkout.
On Tue, May 20, 2014 at 4:21 PM, Robert Bradshaw notifications@github.comwrote:
This would make trivial patches much more expensive--is make not correct for the docs?
— Reply to this email directly or view it on GitHubhttps://github.com/robertwb/sage-patchbot/pull/33#issuecomment-43631822 .
One of many examples: http://patchbot.sagemath.org/log/16316/debian/wheezy/sid/x86_64/3.2.0-57-generic/selmer/2014-05-13%2003:47:56%20+0100
jacobi.rst is clearly not from that ticket.
Hmm... maybe this means that /docs should not be considered "safe."
But better than leaving it how it is.
fixes #32