From b9114260f89fb94eb36b554136f1d65822d7c6a9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 2 Jul 2015 10:57:42 -0700
Subject: [PATCH] feat(script/lib_perf): use gtime if time doesn't work

---
 script/lib_perf.sh | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/script/lib_perf.sh b/script/lib_perf.sh
index 627a94a1c3..68a07b9d3d 100755
--- a/script/lib_perf.sh
+++ b/script/lib_perf.sh
@@ -4,6 +4,10 @@
 TIME=/usr/bin/time
 REALPATH=realpath
 
+if ! $TIME --format "$rf %e" ls 2> /dev/null > /dev/null; then
+    TIME=gtime
+fi
+
 MY_PATH="`dirname \"$0\"`"
 LEAN=$MY_PATH/../bin/lean
 LIB=$MY_PATH/../library