From 9bfd812a887e2acac07bff573e91d5bda6143617 Mon Sep 17 00:00:00 2001 From: Norman Feske Date: Tue, 19 Jan 2021 14:17:26 +0100 Subject: [PATCH] tool/run: search repos for run-tool plugins This patch allows for supplementing the existing run-tool plugins with additional plugins hosted inside a repository. E.g., it enables the run tool to find world/tool/run/boot_dir/hw automatically. Fixes #3993 --- tool/run/run | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/tool/run/run b/tool/run/run index bbf33c35ab..0e8603d7f4 100755 --- a/tool/run/run +++ b/tool/run/run @@ -1056,14 +1056,15 @@ foreach include_name [get_cmd_arg --include ""] { continue } - # if it is relative, check run modules - set run_path [genode_dir]/tool/run - set dir { etc } - lappend dir $run_path + # if it is relative, check repositories and tool directory for run modules + set search_dirs {} + foreach rep_dir $repositories { + lappend search_dirs [file join $rep_dir tool run] } + lappend search_dirs [genode_dir]/tool/run set found 0 - foreach location $dir { - set include_file $location/$include_name + foreach dir $search_dirs { + set include_file $dir/$include_name if {[file exists $include_file] == 1} { puts "including $include_file" lappend include_list $include_name @@ -1071,7 +1072,6 @@ foreach include_name [get_cmd_arg --include ""] { set found 1 break - } else { } }