Update an error that got missed

There was an error that was fixed previously, but it did not get to be
pushed to the repository. It has been fixed now and it will be pushed.