66fde9e6b7
This seems to have just been an inadvertent mistake when copy-pasting. This commit just removes an annoying warning.