Decimal floating point can also start with 0. 0e 0E

A floating point number starting with 0. 0e or 0E is still decimal.
Make it easier by falling back to the standard decimal conversion
routine for anything not recognized as a radix prefix.

float.c

@@ -676,16 +676,9 @@ static int to_float(const char *str, int sign, uint8_t * result,
 	    case 't': case 'T':
 		ok = ieee_flconvert(str+2, mant, &exponent);
 		break;
-	    case '0': case '1': case '2': case '3': case '4':
-	    case '5': case '6': case '7': case '8': case '9':
-	    case '\0':
-		/* Leading zero was just a zero */
-		ok = ieee_flconvert(str, mant, &exponent);
-		break;
 	    default:
-		error(ERR_NONFATAL,
-		      "floating-point constant: invalid radix `%c'", str[1]);
-		ok = false;
+		/* Leading zero was just a zero? */
+		ok = ieee_flconvert(str, mant, &exponent);
 		break;
 	    }
 	} else if (str[0] == '$') {