diff --git a/base-common/duneci-install-module b/base-common/duneci-install-module index d2ae61633edace02786649070c72b7481ecf2cb6..f2bf90a7497a2e772702d8258cfde1460f3f38ad 100755 --- a/base-common/duneci-install-module +++ b/base-common/duneci-install-module @@ -74,7 +74,7 @@ opts="${DUNECI_OPTS:-/duneci/opts.gcc}" ( cd "${module}" - git_branch=$(git symbolic-ref HEAD) + git_branch=$(git symbolic-ref HEAD 2>/dev/null || echo "(unknown)") git_branch="${git_branch#refs/heads/}" echo echo "Installing ${module}; branch ${git_branch}"