From 8a1a30befafffdc07803a0153bf92b469e5b3c2a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Alejandro=20Criado-P=C3=A9rez?= Date: Sat, 19 Aug 2023 13:41:30 +0200 Subject: [PATCH] Added git installed check --- scripts/build.sh | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/scripts/build.sh b/scripts/build.sh index 3d63db29d..7466bb1e7 100755 --- a/scripts/build.sh +++ b/scripts/build.sh @@ -1,6 +1,12 @@ #!/usr/bin/env bash set -e +# Check if git is installed +if ! command -v git &> /dev/null; then + echo "Error: git is not installed. Please install git and try again." + exit 1 +fi + ROOTDIR="$(dirname "$0")/.." BUILDDIR="${ROOTDIR}/build" @@ -10,6 +16,7 @@ else BUILD_TYPE="$1" fi +# Check the first git tag that points to the current commit and starts with "v" if [[ "$(git tag --points-at HEAD 2>/dev/null | head -n 1)" == v* ]]; then touch "${ROOTDIR}/prerelease.txt" fi