diff options
| author |  Joey Hess <joey@kitenet.net> | 2013-08-21 18:17:48 -0400 |
|---|---|---|
| committer | Joey Hess <joey@kitenet.net> | 2013-08-21 18:17:48 -0400 |
| commit | 813f94706e0f4c9afa529f1eabe3f4100f45b50d (patch) | |
| tree | e621cc4bda838c10e2f965a4f226df36b8a72412 | |
| parent | 08b906fa942f6032d4150a419976489193edb18a (diff) | |
Revert "Delete empty downloaded file when wget fails, to work around reported resume failure."
This reverts commit 845322a564fe9ff098596f419d06ec9aa748aa2a.
Better fix forthcoming
| -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 |