diff options
Diffstat (limited to 'tools/ci/jobs/pages.sh')
| -rwxr-xr-x | tools/ci/jobs/pages.sh | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/tools/ci/jobs/pages.sh b/tools/ci/jobs/pages.sh new file mode 100755 index 000000000..2c12253db --- /dev/null +++ b/tools/ci/jobs/pages.sh @@ -0,0 +1,20 @@ +#!/bin/bash + +export LOGFILE=pages.log + +source ./tools/ci/scripts/init.sh + +aptget_install git-core + +tools/ci/scripts/retry.sh git clone https://gitlab.com/4144/pagesindexgen.git pagesindexgen + +mkdir -p public/docs +mkdir -p public/stats + +cd pagesindexgen +./pagesindexgen.py ../public + +cd .. +cp -r doxygen/html/* public/docs +cp -r stats/* public/stats + |