From 0ec480b6c974d8ef9291679695b560f2a5c910f8 Mon Sep 17 00:00:00 2001
From: Andre Anjos <andre.dos.anjos@gmail.com>
Date: Mon, 7 Jun 2021 16:45:50 +0200
Subject: [PATCH] [scripts.mirror] Allow whitelisting to take precedence
---
bob/devtools/scripts/mirror.py | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/bob/devtools/scripts/mirror.py b/bob/devtools/scripts/mirror.py
index 9fc0e863..fcd9de0c 100644
--- a/bob/devtools/scripts/mirror.py
+++ b/bob/devtools/scripts/mirror.py
@@ -246,7 +246,7 @@ def mirror(
if whitelist is not None and os.path.exists(whitelist):
globs_to_consider = set(load_glob_list(whitelist))
- to_download = whitelist_filter(to_download, globs_to_consider)
+ to_download += whitelist_filter(remote_packages, globs_to_consider)
# in the local packages, subset those that we no longer need, be it
# because they have been removed from the remote repository, or because
--
GitLab