diff options
| -rwxr-xr-x | scripts/change.sh | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/scripts/change.sh b/scripts/change.sh index 8b8ab92b..dcd581ee 100755 --- a/scripts/change.sh +++ b/scripts/change.sh @@ -14,6 +14,7 @@ mkdir -p "$PREFIX" || exit 1 for i in $(generated/instlist | egrep -vw "sh|help") do - echo -n "$i " && - scripts/single.sh $i > /dev/null || touch $PREFIX/${i}.bad + echo -n " $i" && + scripts/single.sh $i > /dev/null 2>$PREFIX/${i}.bad && + rm $PREFIX/${i}.bad || echo -n '*' done |