diff options
Diffstat (limited to 'tools/ci/jobs/pages.sh')
| -rwxr-xr-x | tools/ci/jobs/pages.sh | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/tools/ci/jobs/pages.sh b/tools/ci/jobs/pages.sh index 2c12253db..0e3c2b020 100755 --- a/tools/ci/jobs/pages.sh +++ b/tools/ci/jobs/pages.sh @@ -4,15 +4,20 @@ export LOGFILE=pages.log source ./tools/ci/scripts/init.sh -aptget_install git-core +aptget_install git-core python tools/ci/scripts/retry.sh git clone https://gitlab.com/4144/pagesindexgen.git pagesindexgen mkdir -p public/docs mkdir -p public/stats +mkdir -p public/gcov + +cp logs/gcc-6.* public/gcov +cp logs/gcc-6_SDL2.* public/gcov cd pagesindexgen ./pagesindexgen.py ../public +check_error $? cd .. cp -r doxygen/html/* public/docs |