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