{
    "mode": "info",
    "parameter": "dvitomp",
    "section": "",
    "url": "https://www.chedong.com/phpMan.php/info/dvitomp/json",
    "generated": "2026-07-30T12:24:27Z",
    "sections": {
        "File: web2c.info,  Node: dvitomp invocation,  Prev: Initial MetaPost,  Up: MetaPost": {
            "content": "",
            "subsections": [
                {
                    "name": "7.3 DVItoMP: DVI to MPX conversion",
                    "content": "DVItoMP converts DVI files into low-level MetaPost commands in a\nso-called MPX file.  Synopsis:\n\ndvitomp DVIFILE[.dvi] [MPXFILE[.mpx]]\n"
                }
            ]
        },
        "If MPXFILE is not specified, the output goes to the basename of DVIFILE": {
            "content": "extended with '.mpx', e.g., 'dvitomp /wherever/foo.dvi' creates\n'./foo.mpx'.\n\nDVItoMP supports Dvips-style color specials, such as 'color push\nNAME' and 'color pop', outputting them as 'withcolor' MetaPost commands.\n\nThe only options are '-help' and '-version' (*note Common options::).\n",
            "subsections": []
        }
    },
    "flags": [],
    "examples": [],
    "see_also": []
}