changeset 4505:81a47962536a

Make GUB_DOWNLOAD_CACHE separate argument, optionally prepend file://.
author Jan Nieuwenhuizen <janneke@gnu.org>
date Sat, 25 Oct 2008 10:13:07 +0200
parents 014735e1e70f
children 745ab57602c6
files gub/misc.py
diffstat 1 files changed, 6 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/gub/misc.py	Sat Oct 25 09:54:30 2008 +0200
+++ b/gub/misc.py	Sat Oct 25 10:13:07 2008 +0200
@@ -202,7 +202,8 @@
 
 # FIXME: read settings.rc, local, fallback should be a user-definable list
 def download_url (original_url, dest_dir,
-                  local=os.environ.get ('GUB_DOWNLOAD_CACHE', '').split (':'),
+                  local=[],
+                  cache=[os.environ.get ('GUB_DOWNLOAD_CACHE', '')],
                   fallback=['http://lilypond.org/download/gub-sources'],
                   progress=sys.stderr.write):
 
@@ -210,8 +211,10 @@
     assert type (fallback) == list
 
     candidate_urls = []
-    for url in local + [original_url] + fallback:
-        if url and not url.endswith ('gub-sources'):
+    for url in local + cache + [original_url] + fallback:
+        if url and os.path.exists (url):
+            url = 'file://' + url
+        if url == original_url:
             candidate_urls.append (url)
         if not is_ball (os.path.basename (url)):
             candidate_urls.append (rewrite_url (original_url, url))