Where is settings.pantheon.php docummented?

[beto-aveiga]

I couldn't find documentation for settings.pantheon.php

We are copying it if we detect we are using Pantheon, but I don't see if we are including it automatically (modifying settings.php file, I don't think so 🤔 ) or if we expect the user to include it on the settings.php.

https://github.com/Lullabot/drainpipe/blob/db84b66a2a5ce7aa0cec5b30f4f0e834d6bc9cc6/src/ScaffoldInstallerPlugin.php#L294