# HG changeset patch
# User Chris Cannam
# Date 1549540587 0
# Node ID 85e84012311bd7ed7257ce137625b6bcfd00bd34
# Parent  d659ed4b9197ae6e20ea11f2497d91a3eb9e0ebd
Don't really want to run "time" here

diff -r d659ed4b9197 -r 85e84012311b SCRIPTS/process.sh
--- a/SCRIPTS/process.sh	Thu Feb 07 11:48:53 2019 +0000
+++ b/SCRIPTS/process.sh	Thu Feb 07 11:56:27 2019 +0000
@@ -442,7 +442,7 @@
                 continue
             fi
 	    echo "Running command: VAMP_PATH=\"$pdir\" $hostwrapper vamp-plugin-tester/vamp-plugin-tester$hostext \"$extra\" -t \"$test\" \"$id\"" | tee -a "$log"
-	    if ( VAMP_PATH="$pdir$sep./vampy" time $hostwrapper vamp-plugin-tester/vamp-plugin-tester$hostext "$extra" -t "$test" "$id" 2>&1 | tee -a "$log" ; exit ${PIPESTATUS[0]} ) ; then
+	    if ( VAMP_PATH="$pdir$sep./vampy" $hostwrapper vamp-plugin-tester/vamp-plugin-tester$hostext "$extra" -t "$test" "$id" 2>&1 | tee -a "$log" ; exit ${PIPESTATUS[0]} ) ; then
 	        echo "OK" | tee -a "$log"
 	    else
                 if [ -n "$do_speedy" ]; then