Send patches - preferably formatted by git format-patch - to patches at archlinux32 dot org.
summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorErich Eckner <git@eckner.net>2018-12-07 10:47:10 +0100
committerErich Eckner <git@eckner.net>2018-12-07 10:47:10 +0100
commit2fc12361785c7e874c25d6e79f73b76300fc0cbe (patch)
tree3b0115503f0bfec7a9fa7c47c14a87f4b92757a7
parentabb2577a236d648eae3904debaf6e7e59146f873 (diff)
lib/helper.php: site_is_reachable() new
-rw-r--r--lib/helper.php16
1 files changed, 16 insertions, 0 deletions
diff --git a/lib/helper.php b/lib/helper.php
index 84cb69c..05ff2e1 100644
--- a/lib/helper.php
+++ b/lib/helper.php
@@ -169,3 +169,19 @@ function if_unset($array, $index, $default) {
else
return $default;
};
+
+function site_is_reachable($url) {
+ $scd = stream_context_get_default();
+ stream_context_set_default(array('timeout' => 1));
+ $headers = get_headers($url);
+ stream_context_set_default($scd);
+ if (is_array($headers))
+ foreach ($headers as $header) {
+ if (!(strpos($header, 'HTTP/') === 0))
+ continue;
+ if ($header[1] == '200')
+ return true;
+ return false;
+ }
+ return false;
+}