On 12/11/2013 12:17 AM, WaddleSplash wrote:
Shouldn't these repos be deleted? They've both been merged into their upstream counterparts, and I see no reason to keep them around anymore.
Indeed. Done. CU, Ingo