diff --git a/TOOLS/idet.sh b/TOOLS/idet.sh index e9214ef844..ae7a3612fe 100755 --- a/TOOLS/idet.sh +++ b/TOOLS/idet.sh @@ -47,7 +47,7 @@ judge() progressive=$((progressive + progressive1)) undetermined=$((undetermined + undetermined1)) done <