diff options
| author | Michael Niedermayer <michael@niedermayer.cc> | 2019-02-22 00:12:10 +0300 |
|---|---|---|
| committer | Michael Niedermayer <michael@niedermayer.cc> | 2019-03-02 01:25:08 +0300 |
| commit | b7140a4db574d9669d955aba5283f2a5c7ec23f2 (patch) | |
| tree | 4fec2b3a262331ceb83d08073936e92e95becfa8 /tools/target_dec_fate.sh | |
| parent | 4801eea0d465cd54670e7c19322705544e3e7524 (diff) | |
tools/target_dec_fate.sh: Add support for lines that are comments
Signed-off-by: Michael Niedermayer <michael@niedermayer.cc>
Diffstat (limited to 'tools/target_dec_fate.sh')
| -rwxr-xr-x | tools/target_dec_fate.sh | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/tools/target_dec_fate.sh b/tools/target_dec_fate.sh index 1fdfdcaaea..1377b6b4e8 100755 --- a/tools/target_dec_fate.sh +++ b/tools/target_dec_fate.sh @@ -50,6 +50,8 @@ while read -r LINE; do FILE=`echo $LINE | sed 's# .*##'` if test -f "$1/$FILE" ; then echo exists $FILE + elif echo "$ISSUE_NUM" | grep '#' >/dev/null ; then + echo disabled $FILE else echo downloading $FILE mkdir -p "$1/$ISSUE_NUM" @@ -72,6 +74,9 @@ make -j4 $TOOLS while read -r LINE; do TOOL_ID=`echo $LINE | sed 's#[^ ]* ##'` FILE=`echo $LINE | sed 's# .*##'` + if ! test -f "$1/$FILE" ; then + continue + fi tools/$TOOL_ID $1/$FILE done < "tools/$LIST" |