#200424 by mpare and myself: strengten the note that all settings.php set configuration options are fixed, and cannot be modified on the web interface