diff options
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/ci/jobs/pages.sh | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/tools/ci/jobs/pages.sh b/tools/ci/jobs/pages.sh index 79acc67ff..fa3f992f0 100755 --- a/tools/ci/jobs/pages.sh +++ b/tools/ci/jobs/pages.sh @@ -9,9 +9,13 @@ tools/ci/scripts/retry.sh git clone https://gitlab.com/4144/pagesindexgen.git pa mkdir -p public/docs mkdir -p public/stats mkdir -p public/gcov +mkdir -p public/version cp logs/gcc-6.* public/gcov cp logs/gcc-6_SDL2.* public/gcov +echo "Url: $CI_PROJECT_URL" >public/version/commit.txt +echo "Ref name: $CI_BUILD_REF_NAME" >>public/version/commit.txt +echo "Ref: $CI_BUILD_REF" >>public/version/commit.txt cd pagesindexgen ./pagesindexgen.py ../public |