mirror of
https://github.com/genodelabs/genode.git
synced 2025-02-20 09:46:20 +00:00
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
This commit is contained in:
parent
1ccf8a280c
commit
9bfd812a88
14
tool/run/run
14
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 {
|
||||
}
|
||||
}
|
||||
|
||||
|
Loading…
x
Reference in New Issue
Block a user