This has recurred, and I have realised that it's the restart of Apache that fixes it, not the edit to config.php [which necessitated the restart].
This has recurred, and I have realised that it's the restart of Apache that fixes it, not the edit to config.php [which necessitated the restart].