From 2fdaec0c683a6b140a28cef1d1b2a32b352f4696 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Wed, 4 Jul 2018 04:02:02 +0200
Subject: [ci] Avoid annoying detached head warning.

---
 dev/ci/ci-common.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

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')" )
 }
 
-- 
cgit v1.2.3