Hi *, I’ve had a look at this again. Helmut had suggested that I split the installed trees between core and extensions into two separate directories (instead of combining them into one directory with entries being sometimes symlinks, sometimes directories, under /var/lib/mediawiki/extensions), but this would be futile: hundreds of files (in core, core-extensions and extra-extensions) hardcode the path.
I shall be trying something else. bye, //mirabilos -- tarent solutions GmbH Rochusstraße 2-4, D-53123 Bonn • http://www.tarent.de/ Tel: +49 228 54881-393 • Fax: +49 228 54881-314 HRB 5168 (AG Bonn) • USt-ID (VAT): DE122264941 Geschäftsführer: Boris Esser, Sebastian Mancke -- To UNSUBSCRIBE, email to debian-bugs-rc-requ...@lists.debian.org with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org