From 38d014d19696306328daba02f023bc9c35065185 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Fri, 28 May 2021 12:56:22 -0700 Subject: [PATCH] ignore --ignore-cr-at-eol for old gits --- .scripts/release-pre.sh | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/.scripts/release-pre.sh b/.scripts/release-pre.sh index 1d8fe08cc2d..e24b654bf31 100644 --- a/.scripts/release-pre.sh +++ b/.scripts/release-pre.sh @@ -32,8 +32,10 @@ if ! [[ -d ulib ]]; then fi # Fail if the state is dirty -git diff --staged --exit-code --ignore-cr-at-eol -git diff --exit-code --ignore-cr-at-eol +# NOTE: --ignore-cr-at-eol is a recent option, +# so we should ignore it if it is not there +git diff --staged --exit-code --ignore-cr-at-eol || git diff --staged --exit-code +git diff --exit-code --ignore-cr-at-eol || git diff --exit-code # Detect the F* version number git fetch --tags $git_remote