aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--dev/ci/ci-common.sh2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 85df249d3..a68cd0933 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -69,7 +69,7 @@ git_checkout()
if [ ! -d .git ] ; then git clone "${_DEPTH[@]}" "${_URL}" . ; fi && \
echo "Checking out ${_DEST}" && \
git fetch "${_URL}" "${_BRANCH}" && \
- git checkout "${_COMMIT}" && \
+ git -c advice.detachedHead=false checkout "${_COMMIT}" && \
echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" )
}