#ifndef lint
static char patchlevel[] = "@(#) patchlevel 7.2";
#endif