Thanks Bartosz and others who replied
It was indeed a resource loader migration issue. Suitable changes to Common.js fixed it.
Peter Presland
On 17/06/2019 19:25, Bartosz Dziewoński wrote:
Looks like this problem to me:
https://www.mediawiki.org/wiki/ResourceLoader/Migration_guide_(users)#Avoid_...)