efc3e28c31
This patch fixes a PHP lint error introduced in MDL-75552. As this issue was closed a few weeks ago, I'm adding it to one random issue integrated this week. Thanks Eloy and Paul for your help! :-*