compare_testfiles.sh: explicitly specify output format for time; different systems (shells) use different things...

3 years ago · 0af164582f
parent ab9382ea4a
commit 0af164582f
1 changed files with 3 additions and 1 deletions
--- a/tests/compare_testfiles.sh
+++ b/tests/compare_testfiles.sh
@ -1,6 +1,8 @@
 #!/bin/sh

-if [ "$1" = "" ]; then 
+export TIME='real\t  %e'
+
+if [ "$1" = "" ]; then
 	echo "specify path to tlc binary"
 	exit 1
 else