It eventually turned out our admin had moved the wiki directory to a new location while leaving the old copy in place. Thus I was editing a localsettings.php to no effect... Sorry for the false alarm, and thank you for the (as always) kind and patient response.
