hack to work around gcc 4.2 compiler warning; really we should not store static strings in char * pointers (they should all be changed to const char *).