I am going to close this one, after a second look at it, seems to be specific to your case, because it looks at the default server profile only, also it does not check if server_name is set or not, because it is not a mandatory field.

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub, or unsubscribe.
Triage notifications on the go with GitHub Mobile for iOS or Android.