diff options
Diffstat (limited to 'script')
| -rwxr-xr-x | script/trees | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/script/trees b/script/trees index 21f05e5d..c806b92a 100755 --- a/script/trees +++ b/script/trees @@ -59,6 +59,7 @@ build_projects() [ -f "$listfile" ] || listfile="" # optional on single-tree dest_dir="$elfdir" + elfcheck || return 0 cdir="src/${project}" [ -d "$cdir" ] || x_ ./update trees -f "$project" @@ -175,11 +176,17 @@ check_config() [ -f "$config" ] || $err "check_config $project/$target: no config" dest_dir="$elfdir/$target/$config_name" + elfcheck || return 1 # skip build if a previous one exists + + x_ mkdir -p "$dest_dir" +} + +elfcheck() +{ # TODO: very hacky check. do it properly (based on build.list) for elftest in "$dest_dir"/*; do e "$elftest" f && return 1 done - x_ mkdir -p "$dest_dir" } handle_makefile() |