Problems parsing numbers written with the _ format

[ralphtheninja]

tinyify has some problems parsing numbers written like 10_000:

SyntaxError: Unexpected token name «_000», expected punc «,» while parsing file: /home/lms/src/peermaps/peermaps-web/storage/http.js
    at Z.get (/home/lms/src/peermaps/peermaps-web/node_modules/uglifyify/node_modules/terser/dist/bundle.min.js:1:463)
    at Readable.errorExit (/home/lms/src/peermaps/peermaps-web/node_modules/browserify/bin/cmd.js:79:27)
    at Readable.emit (node:events:526:28)
    at Labeled.<anonymous> (/home/lms/src/peermaps/peermaps-web/node_modules/read-only-stream/index.js:28:44)
    at Labeled.emit (node:events:526:28)
    at Labeled.<anonymous> (/home/lms/src/peermaps/peermaps-web/node_modules/stream-splicer/index.js:130:18)
    at Labeled.emit (node:events:526:28)
    at Deps.<anonymous> (/home/lms/src/peermaps/peermaps-web/node_modules/stream-splicer/index.js:130:18)
    at Deps.emit (node:events:526:28)
    at DuplexWrapper.<anonymous> (/home/lms/src/peermaps/peermaps-web/node_modules/module-deps/index.js:414:22)

[ralphtheninja]

I can fix this on my side by changing it to 10000, so nothing crucial to fix.