const char* version() { const char* s = "Revision: 1992M"; return s; }