On Sat, Jul 12, 2014 at 6:56 AM, Jeff King wrote: > I think none of the regular devs uses PROFILE, and it bit-rotted By the way, is there no build (CI) server for git.git to regularly test branches on different platforms or at least different build configs on the same platform? -- To unsubscribe from this list: send the line "unsubscribe git" in the body of a message to majordomo@xxxxxxxxxxxxxxx More majordomo info at http://vger.kernel.org/majordomo-info.html