web2c: dvitomp invocation

 
 7.3 DVItoMP: DVI to MPX conversion
 ==================================
 
 DVItoMP converts DVI files into low-level MetaPost commands in a
 so-called MPX file.  Synopsis:
 
      dvitomp DVIFILE[.dvi] [MPXFILE[.mpx]]
 
 If MPXFILE is not specified, the output goes to the basename of DVIFILE
 extended with '.mpx', e.g., 'dvitomp /wherever/foo.dvi' creates
 './foo.mpx'.
 
    DVItoMP supports Dvips-style color specials, such as 'color push
 NAME' and 'color pop', outputting them as 'withcolor' MetaPost commands.
 
    The only options are '-help' and '-version' (⇒Common options).