summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJérôme.Vouillon <jvouillon@besport.com>2019-08-14 18:11:40 +0200
committerThomas Refis <refis.thomas@gmail.com>2019-08-16 16:49:59 +0100
commitdceeb8301f68a92ae9c739813eb842c4b153a08f (patch)
tree0539e9d9ad3b7735f3005cbec785ed69c79d7a9b
parent1c1865d4839f72e52319fb86975a02b66088783b (diff)
downloadocaml-dceeb8301f68a92ae9c739813eb842c4b153a08f.tar.gz
Fix tool check-parser-uptodate-or-warn.sh
Improve detection of stat supported options
-rwxr-xr-xtools/check-parser-uptodate-or-warn.sh6
1 files changed, 3 insertions, 3 deletions
diff --git a/tools/check-parser-uptodate-or-warn.sh b/tools/check-parser-uptodate-or-warn.sh
index 5502eae549..86620a23a4 100755
--- a/tools/check-parser-uptodate-or-warn.sh
+++ b/tools/check-parser-uptodate-or-warn.sh
@@ -24,14 +24,14 @@
# seconds after boot/menhir/parser.ml.
# mtime(): access a file's last modification time as a timestamp,
-# using either GNU coreutils' stat --format, or BSD/macos stat -f.
+# using either GNU coreutils' stat -c, or BSD/macos stat -f.
# Default to 0 if 'stat' is not available.
stat . 2>/dev/null 1>/dev/null
if test $? != 0
then MTIME=""
-elif test -n "$(stat --version 2>/dev/null | grep coreutils)"
-then MTIME="stat --format %Y"
+elif stat -c %Y . 2>/dev/null 1>/dev/null
+then MTIME="stat -c %Y"
else MTIME="stat -f %m"
fi