diff --git a/.github/jobs/baseinstall.sh b/.github/jobs/baseinstall.sh index f19ee5fc4d..9403a49124 100755 --- a/.github/jobs/baseinstall.sh +++ b/.github/jobs/baseinstall.sh @@ -54,6 +54,7 @@ else --enable-judgehost-build=no | tee "$ARTIFACTS"/configure.txt make domserver make install-domserver + cp -r ${DIR}/doc /opt/domjudge/domserver/ fi section_end