Hello!
I need to shut down the tools-dev host in order to move it to a different server. The downtime will be brief, but in the meantime I recommend people move their work to a different bastion (e.g. tools-login.wmflabs.org) in order to avoid interruption.
This will happen on or near 15:00 UTC on Tuesday, 2018-11-20. I'll also send alerts to sessions on the bastion prior to the shutdown.
-Andrew