run-dev: Automatically set EXTERNAL_HOST for droplet dev servers.

As of commit 99242138a7 (#14530), this
is required when visiting a droplet dev server remotely.

Signed-off-by: Anders Kaseorg <anders@zulipchat.com>

tools/run-dev.py

@@ -4,6 +4,7 @@ import argparse
 import os
 import pwd
 import signal
+import socket
 import subprocess
 import sys
 import traceback
@@ -78,6 +79,8 @@ if options.interface is None:
         # host.  The same argument applies to the remote development
         # servers using username "zulipdev".
         options.interface = None
+        if user_name == "zulipdev":
+            os.environ.setdefault("EXTERNAL_HOST", socket.gethostname() + ":9991")
     else:
         # Otherwise, only listen to requests on localhost for security.
         options.interface = "127.0.0.1"