From 67869a697bab257fca663017c591da99e00f285c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Josef=20S=C3=B6ntgen?= Date: Tue, 9 Jan 2018 13:37:18 +0100 Subject: [PATCH] run: add deport-dir argument By specifying '--depot-dir' in the RUN_OPTS it is possible to override the default depot ($GENODE_DIR/deport) location with the given path. --- tool/run/depot.inc | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/tool/run/depot.inc b/tool/run/depot.inc index e34c9ed2e..4901c1f98 100644 --- a/tool/run/depot.inc +++ b/tool/run/depot.inc @@ -4,7 +4,15 @@ # \date 2017-03-29 # -proc depot_dir { } { return [genode_dir]/depot } +# +# Return depot directory path +# +# \param --depot-dir set depot directory to given path, otherwise +# default value [genode_dir]/depot is used +# +proc depot_dir { } { + return [get_cmd_arg_first --depot-dir "[genode_dir]/depot"] +} ##