On Mon, Mar 26, 2012 at 3:43 PM, Thomas Gries <mail(a)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.