isonum_712
static __inline int isonum_712(char *) __attribute__ ((__unused__));
return isonum_712((signed char *)buf);