diff options
| author | Erich Eckner <git@eckner.net> | 2019-07-15 09:26:36 +0200 |
|---|---|---|
| committer | Erich Eckner <git@eckner.net> | 2019-07-15 09:26:36 +0200 |
| commit | 88f4f2f1e139ffee213a23dee4f26cf6ec2ae637 (patch) | |
| tree | ae47af9aeba80ba0f16513cc22a91719f61f3ef4 | |
| parent | d46e90ab1e8219ff89cb56ad0d894958139672f0 (diff) | |
| download | sourceMirror-88f4f2f1e139ffee213a23dee4f26cf6ec2ae637.tar.xz | |
mirror.php: set user-agent in curl
| -rw-r--r-- | mirror.php | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -70,7 +70,7 @@ passthru( "mkdir -p '".dirname($pfad)."'; ". "( ". - "curl -Ls '".$quelle."' || ". + "curl -Ls -A "Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Firefox/68.0" '".$quelle."' || ". "wget -O - '".$quelle."'; ". ") | ". // oder curl! "tee \"".$pfad."\"" |