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"] +} ##