diff options
| -rw-r--r-- | Utility/Url.hs | 12 | ||||
| -rw-r--r-- | debian/changelog | 2 |
2 files changed, 2 insertions, 12 deletions
diff --git a/Utility/Url.hs b/Utility/Url.hs index c877583d8..508b9eeb4 100644 --- a/Utility/Url.hs +++ b/Utility/Url.hs @@ -118,16 +118,8 @@ download' quiet url headers options file = - downloaded before the resume. -} curl = go "curl" $ headerparams ++ quietopt "-s" ++ [Params "-f -L -C - -# -o"] - go cmd opts = do - ok <- boolSystem cmd $ - options++opts++[File file, File url] - -- wget sometimes leaves behind an empty file on failure; - -- remove this as it sometimes interferes with a re-download - unless ok $ do - size <- catchMaybeIO $ fileSize <$> getFileStatus file - when (size == Just 0) $ - removeFile file - return ok + go cmd opts = boolSystem cmd $ + options++opts++[File file, File url] quietopt s | quiet = [Param s] | otherwise = [] diff --git a/debian/changelog b/debian/changelog index 359a052f2..cc60b973b 100644 --- a/debian/changelog +++ b/debian/changelog @@ -7,8 +7,6 @@ git-annex (4.20130816) UNRELEASED; urgency=low * import: Add options to control handling of duplicate files: --duplicate, --deduplicate, and --clean-duplicates * mirror: New command, makes two repositories contain the same set of files. - * Delete empty downloaded file when wget fails, to work around reported - resume failure. -- Joey Hess <joeyh@debian.org> Thu, 15 Aug 2013 15:47:52 +0200 |