Le 07/04/12 09:38, Antoine Musso a écrit :
PHP linter is enabled on mediawiki/core.git as of April 8th. It is implemented as a Jenkins job running php -l on any file which have been modified.
Isn't it also linting merges? It didn't detect the merge today of a broken patchset it had verified before (c4368).