mirror.php: use curl and wget

1 files changed, 4 insertions, 1 deletions

diff --git a/mirror.php b/mirror.php
index 09172bd..8afc56a 100644
--- a/mirror.php
+++ b/mirror.php
@@ -56,7 +56,10 @@
     if (! file_exists($pfad)) {
       passthru(
         "mkdir -p '".dirname($pfad)."'; ".
-        "wget -O - '".$quelle."' | ". // oder curl!
+        "( ".
+        "curl -Ls '".$quelle."' || ".
+        "wget -O - '".$quelle."'; ".
+        ") | ". // oder curl!
           "tee \"".$pfad."\""
       );
     }