On Mon, Mar 26, 2012 at 3:43 PM, Thomas Gries mail@tgries.de wrote:
Much better approach: to find a "live" way to have separate links - for extensions with and without repos in git !
Yes, you can do that after you revert the change that breaks a large percentage of the extension links.