| commit | d8398820f182ddc9255b8bff2ee5fe52097e22b8 | [log] [tgz] |
|---|---|---|
| author | Davide Pesavento <davidepesa@gmail.com> | Sun Mar 29 18:46:19 2020 -0400 |
| committer | Davide Pesavento <davidepesa@gmail.com> | Sun Mar 29 21:39:11 2020 -0400 |
| tree | b037da4494d2725e7723a6220a7b72a48b97cf46 | |
| parent | a1a9d704bad78b34cd18b59dcb1b92690c72b8e0 [diff] [blame] |
ci: add CentOS 8 support; drop CentOS 7 Refs: #5040, #5087 Change-Id: Ia680fecc41d16d21d7b03f117a30a2966cf46679
diff --git a/.jenkins.d/10-build.sh b/.jenkins.d/10-build.sh index ccbcc93..f5ef90a 100755 --- a/.jenkins.d/10-build.sh +++ b/.jenkins.d/10-build.sh
@@ -1,10 +1,5 @@ #!/usr/bin/env bash -set -e - -JDIR=$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd ) -source "$JDIR"/util.sh - -set -x +set -ex git submodule sync git submodule update --init