From: Daniel Arndt <daniel.arndt@iwr.uni-heidelberg.de>
Date: Sun, 20 May 2018 19:55:59 +0000 (+0200)
Subject: Merge pull request #6635 from bangerth/use-wget
X-Git-Tag: v9.1.0-rc1~1123
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=414611ba21e0528b4439d4937a9b3134a40c66a0;p=dealii.git

Merge pull request #6635 from bangerth/use-wget

Use wget instead of curl.
---

414611ba21e0528b4439d4937a9b3134a40c66a0