Handle file:// URLs. Close #37

2025-11-22 11:46:53 +00:00 · 2016-04-16 09:10:00 +02:00
parent ce44ffe266
commit 3aeb71b204
1 changed files with 4 additions and 0 deletions
--- a/common.py
+++ b/common.py
@ -381,6 +381,10 @@ def fetch(name, url):
    else:
      with cwd(name):
        execute('git', 'pull')
+  elif url.startswith('file'):
+    if not path.exists(name):
+      _, src = url.split('://')
+      copytree(src, name)
  else:
    panic('URL "%s" not recognized!', url)