From 0f1b7b8c34f665164b236739e593181dba88cbd0 Mon Sep 17 00:00:00 2001
From: Erich Eckner <git@eckner.net>
Date: Thu, 11 Jul 2019 13:40:17 +0200
Subject: Revert "bin/sanity-check: do not _ping_ the master mirror (ping does
 not work O.o) - use curl"

This reverts commit 593f865e209831a95a666204e71f5e20fb2df758.

We repaired the `ping` command on the buildmaster.
---
 bin/sanity-check | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/bin/sanity-check b/bin/sanity-check
index 5160142..3813f22 100755
--- a/bin/sanity-check
+++ b/bin/sanity-check
@@ -158,9 +158,9 @@ while [ $# -gt 0 ]; do
           ' | \
           sort -u
       ); do
-        if ! curl -s "http://$(dig +short "${host}" | tail -n1)" >/dev/null 2>&1; then
+        if ! ping -c1 "${host}" >/dev/null 2>&1; then
           if [ ${silence} -le 1 ]; then
-            printf '\nThe master mirror %s is not reachable.\n' \
+            printf '\nThe master mirror %s cannot be pinged.\n' \
               "${host}" | \
               tee -a "${tmp_dir}/messages" >&2
           fi
-- 
cgit v1.2.3