Code moved to git, sorry about the SPAM for those that still subscribe to adonthell-commits! Should have pushed the old stuff before getting notifications enabled. At least it's confirmed they work! ;-)
> Note that it is possible to have more than one git branch that doesn't
> start at the same history point.
>
> For example, you might have one branch containing your main tree, and
> another branch containing only some support scripts. If you look at
> the full git-log history of both branches, they need not touch each other
> at all.
In the end, I figured that perhaps the simplest solution would also be the best. While the two repositories now have slightly different URLs, in practice it shouldn't be a big deal. And locally, one is free to name the directories whatever one wants anyway.
Kai