diff options
Diffstat (limited to 'tests/tools/autotest.sh')
| -rwxr-xr-x | tests/tools/autotest.sh | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh index d0b0a89d7..d6216244f 100755 --- a/tests/tools/autotest.sh +++ b/tests/tools/autotest.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash libs="" genvcd=false @@ -100,7 +100,7 @@ do echo -n "Test: $bn " fi - rm -f ${bn}.{err,log,sikp} + rm -f ${bn}.{err,log,skip} mkdir -p ${bn}.out rm -rf ${bn}.out/* |