I hadn't noticed this before. On the one hand I could exclude libraries (perhaps better on a case by case basis just so we are aware), on the other hand it's not completely clear to me what the library is for given the native json_* functions?

PHP Deprecated:  Methods with the same name as their class will not be constructors in a future version of PHP; Services_JSON has a deprecated constructor in lib/JSON.php on line 119
PHP Deprecated:  Methods with the same name as their class will not be constructors in a future version of PHP; Services_JSON_Error has a deprecated constructor in lib/JSON.php on line 910
PHP Deprecated:  Methods with the same name as their class will not be constructors in a future version of PHP; Services_JSON_Error has a deprecated constructor in lib/JSON.php on line 924

The JSON library was for the infamous period when php_json was not included in the default PHP distribution on Debian due to a license problem :-/
At some point we should be able to remove it.

And yes, I think third-party libraries should be excluded (and manually checked during inclusion / updates)

Since they're all fine (except for that one) and it is good to be aware of it, I'd argue against a priori exclusion of third-party libraries.

Btw, my local PHP 7.3.3 instance doesn't show this warning. Must be some php.ini setting?

Maybe PHP 7.3.4 (e.g from https://hub.docker.com/_/php ) (I am on mobile atm).
It is indeed good to be aware, so maybe a warning if possible

It's 5.5 or 5.6 7.0 and up on Travis (also mobile here), so definitely not a version thing. :-)

The way I wrote it now only libs/JSON is excluded, to which other files could be added if circumstances require it. The important thing is that it's a conscious decision imo.