const char version_string[] = "dvi2bitmap version 1.0, 2015 January 12";