diff --git a/jenkinsfiles/antora_libraries_1 b/jenkinsfiles/antora_libraries_1 index dbe5703..6d3c31b 100644 --- a/jenkinsfiles/antora_libraries_1 +++ b/jenkinsfiles/antora_libraries_1 @@ -229,6 +229,12 @@ pipeline { pushd $BOOST_ROOT/libs git clone https://github.com/${EXTRA_LIB} -b $BOOST_BRANCH --depth 1 popd + else + # refresh extra lib: + pushd $BOOST_ROOT/libs/${EXTRA_LIB_REPO} + git checkout $BOOST_BRANCH || true + git pull || true + popd fi done diff --git a/scripts/cppalliance_ws_io_prebuild.sh b/scripts/cppalliance_ws_io_prebuild.sh new file mode 100755 index 0000000..47733d1 --- /dev/null +++ b/scripts/cppalliance_ws_io_prebuild.sh @@ -0,0 +1,5 @@ +#!/bin/bash + +set -xe +echo "export PRTEST=prtest3" >> jenkinsjobinfo.sh +echo "export EXTRA_BOOST_LIBRARIES='cppalliance/buffers cppalliance/http_proto cppalliance/ws_proto'" >> jenkinsjobinfo.sh