accidentally put in the *new* url of the *old*, broken repo. :-/
Authored by: michaz 2015-02-18
Parent: [r32208]
Child: [r32210]
