stan/jdk-24
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

8283575: Check for GNU time fails for version >1.7

Browse Source 
Reviewed-by: shade, ihse
This commit is contained in:
Erik Joelsson 2022-03-24 12:48:12 +00:00
parent 2c43ecb43f
commit 1c4f5fcb88
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
make/autoconf/basic_tools.m4
View File

@ -348,7 +348,7 @@ AC_DEFUN_ONCE([BASIC_SETUP_COMPLEX_TOOLS],
UTIL_LOOKUP_PROGS(DTRACE, dtrace, $PATH:/usr/sbin)
UTIL_LOOKUP_PROGS(PATCH, gpatch patch)
# Check if it's GNU time
IS_GNU_TIME=`$TIME --version 2>&1 | $GREP 'GNU time'`
[ IS_GNU_TIME=`$TIME --version 2>&1 | $GREP 'GNU [Tt]ime'` ]
if test "x$IS_GNU_TIME" != x; then
IS_GNU_TIME=yes
else