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"