Undo previous patch; it did not quite work out.