work also in a git-worktree

2018-09-03 16:29:29 +02:00
parent b5474fd02e
commit 6870ddd8ef
1 changed files with 1 additions and 1 deletions
@@ -169,7 +169,7 @@ set -e
 cd ${TMPDIR} || return

 # Update the working copy
-if [ -d "${SOURCES_DIR}/.git" ]; then
+if [ -e "${SOURCES_DIR}/.git" ]; then
    pushd "${SOURCES_DIR}"
    [ -z "$NO_SCM" ] && git pull
    CGAL_GIT_HASH=`git rev-parse HEAD`