diff --git a/data/collect-data.sh.in b/data/collect-data.sh.in index f8b57f5d..94fc1fa6 100755 --- a/data/collect-data.sh.in +++ b/data/collect-data.sh.in @@ -47,6 +47,10 @@ problem_pattern+="\|" problem_pattern+="\|" problem_pattern+="\