From 0af164582f30c8841dc1dd996a77ad7a7e1be1e8 Mon Sep 17 00:00:00 2001
From: Peter Meerwald-Stadler <pmeerw@pmeerw.net>
Date: Tue, 27 Apr 2021 16:09:55 +0200
Subject: [PATCH] compare_testfiles.sh: explicitly specify output format for
 time; different systems (shells) use different things...

---
 tests/compare_testfiles.sh | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tests/compare_testfiles.sh b/tests/compare_testfiles.sh
index 6125bc7..0d6e938 100755
--- 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