mirror of
https://github.com/mmueller41/genode.git
synced 2026-01-21 12:32:56 +01:00
Move depot keys to repos/gems/sculpt/depot
This change keeps the version-controlled 'pubkey' and 'download' files separate from files generated via depot/create or downloaded via depot/download. So one can remove the entire depot/ directory without interfering with git. Furthermore, depot keys can now be hosted in supplemental repositories independent from Genode's main repository. Fixes #4364
This commit is contained in:
committed by
Christian Helmuth
parent
03cbf435e5
commit
f1b46c3205
24
tool/run/run
24
tool/run/run
@@ -572,14 +572,32 @@ proc installed_command {command} {
|
||||
##
|
||||
# Return first repository containing the given path
|
||||
#
|
||||
proc repository_contains {path} {
|
||||
proc repository_contains { rep_rel_path } {
|
||||
|
||||
global repositories;
|
||||
foreach i $repositories {
|
||||
if {[file exists $i/$path]} { return $i }
|
||||
|
||||
foreach rep $repositories {
|
||||
if {[file exists [file join $rep $rep_rel_path]]} {
|
||||
return $rep }
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
##
|
||||
# Return path to first file found in the available repositories
|
||||
#
|
||||
proc select_from_repositories { rep_rel_path } {
|
||||
|
||||
set rep_dir [repository_contains $rep_rel_path]
|
||||
|
||||
if {[llength $rep_dir]} {
|
||||
return [file join $rep_dir $rep_rel_path] }
|
||||
|
||||
puts stderr "Error: $rep_rel_path not present in any repository"
|
||||
exit -8
|
||||
}
|
||||
|
||||
|
||||
##
|
||||
## Utilities for performing steps that are the same on several platforms
|
||||
##
|
||||
|
||||
Reference in New Issue
Block a user