Rob Church wrote :
On 19/06/07, Alexis Moinet alexis.moinet-LfqbaU+xhLyZIoH1IeqzKA@public.gmane.org wrote:
Finally, create a page in your wiki named : Mediawiki:Noexportallowed and put some text in it (e.g. "you must be an admin to use export special page")
The normal method is to call $wgOut->permissionRequired( 'export' );
NB2 : I'm sure I've already seen how to do this in LocalSettings.php without hacking the core code, but I can't remember how (it wasn't a hook it was a kind of function overwriting)
Perhaps conditional removal of the special page if the user doesn't have permission to use it? An example might be http://mediawiki.pastey.net/57133-2mn5.
Thank you Rob
(for the "conditional removal", that's not the solution I was thinking about, but yours is actually simpler and cleaner ;-) )