[this is a good time because the next commit requires workspace rebuild anyway] This was SVN commit r5882.