Description:
------------
When using JSON_NUMERIC_CHECK with json_encode, the behaviour differs starting from php8. I couldn't find if this is documented somewhere, i am also not sure if this is a bug. 

json_encode currently has no option to specify if leading zeros schould be kept. See:
https://bugs.php.net/bug.php?id=79189

This might be correct, since according to the JSON specification, a number cannot start with 0, there is also a bug for this:
https://bugs.php.net/bug.php?id=70680

If some wanted to keep the leading zero, a workaround could be used to add a space character after the number that should keep it's leading zeros.

In php < 8 using JSON_NUMERIC_CHECK:

1. with a whitespace after the number e.g "01234 " it would convert to (string)01234

2. without a whitespace after the number e.g "01234" it would convert to (int)1234

In php >= 8 using JSON_NUMERIC_CHECK:

Whitespaces do not matter, it always converts it to (int)1234.

The behaviour changed, which might be correct. However as stated above i couldn't find this in the changelog or somewhere else documented, maybe it is a bug / unexpected behaviour?


Test script:
---------------
print_r(json_encode('01234 ', JSON_NUMERIC_CHECK));

Expected result:
----------------
"01234 "

Actual result:
--------------
1234