I accidentally wrote the wrong version number.  The right number for
this commit is 0.12.5.