The cpu times are horribly outdated. On modern architectures, processing
of WEB takes fractions of seconds (and few seconds for TEX).