Correct fix in [d084043f79827].  This attempt at fixing the problem is
closed.