From 3033496fa4d344c15cc264b5f9b6fbf044386f67 Mon Sep 17 00:00:00 2001 From: Christian Helmuth Date: Wed, 8 May 2019 13:57:59 +0200 Subject: [PATCH] run: honor DEPOT_DIR for --depot-auto-update Issue #3270 --- tool/run/depot.inc | 1 + 1 file changed, 1 insertion(+) diff --git a/tool/run/depot.inc b/tool/run/depot.inc index 3c59d6985d..10d1556b34 100644 --- a/tool/run/depot.inc +++ b/tool/run/depot.inc @@ -206,6 +206,7 @@ proc _depot_auto_update { archives } { set cmd "[genode_dir]/tool/depot/create $archives_to_create " append cmd "CROSS_DEV_PREFIX=[cross_dev_prefix] " + append cmd "DEPOT_DIR=[depot_dir] " append cmd "UPDATE_VERSIONS=1 FORCE=1 REBUILD= " set make_j_arg ""