Hmph, I did a merge of 'master' into 'ng/master' without pulling first,
so I missed earlier changes to 'ng/master' that were in the central
repository but not in my local repository. Since that merge required
some non-trivial conflicts resolutions, I don't want to redo it; I'm
thus merging the 'ng/master' from the central repository to the local
one "after the fact".