Make HTML the default output format, since that is what people actually

want most of the time.