From c0c9b024b0c9f05385e56c53143732f4b83887f6 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 22 Aug 2023 13:02:45 -0700
Subject: [PATCH] Make `util/make_version` more POSIX-compliant

Fixes #702

I've avoided `&>` as its not POSIX-complaint according to [stack
exchange](https://unix.stackexchange.com/a/590707/45323).

I've also taken the opportunity to simplify slightly the logic that
checks for `git`, relying on the return code of `command -v` rather than
testing that the resulting path exists.

Finally, I've removed the `2>/dev/null` redirect on `command -v`; when the
command does not exist, `command -v` is already silent, and I think we
want noise if `command` itself does not exist or is failing strangely
for some reason.
---
 util/make_version | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/util/make_version b/util/make_version
index aa9d0c8af..ecdc56c6a 100755
--- a/util/make_version
+++ b/util/make_version
@@ -1,8 +1,7 @@
 #!/usr/bin/env bash
 #usage:  util/make_version Bitsize Compcert-version
 F=veric/version.v
-builtin type -P gdate &> /dev/null
-if [ $? -eq 0 ]; then
+if command -v gdate >/dev/null; then
     DATE=gdate
 else
     DATE=date
@@ -10,7 +9,7 @@ fi
 set -e
 printf >$F 'Require Import ZArith Coq.Strings.String. Open Scope string.\n'
 printf >>$F 'Definition git_rev := "'
-if [ -e "$(command -v git)" ] && [ "$(git rev-parse --is-inside-work-tree 2>/dev/null)" = "true" ]; then
+if command -v git >/dev/null && [ "$(git rev-parse --is-inside-work-tree 2>/dev/null)" = "true" ]; then
   git log -n 1 --pretty=format:"%H" >>$F || true
 fi
 printf >>$F '".\n'