/* Disable screen output devices, because the error should
already have been reported to the screen with the
dump_message call above. */
/* Disable screen output devices, because the error should
already have been reported to the screen with the
dump_message call above. */