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