CI updates

This commit is contained in:
WebFreak001 2023-03-22 02:23:43 +01:00
parent 0fd2c13391
commit 20df158917
No known key found for this signature in database
GPG Key ID: AEFC88D11109D1AA
2 changed files with 6 additions and 4 deletions

View File

@ -11,7 +11,7 @@ on:
jobs: jobs:
pr_info: pr_info:
name: PR Info name: PR Info
runs-on: ubuntu-20.04 runs-on: ubuntu-latest
steps: steps:
# we first create a comment thanking the user in pr_info_intro.yml # we first create a comment thanking the user in pr_info_intro.yml
# (separate step due to needing GITHUB_TOKEN access) # (separate step due to needing GITHUB_TOKEN access)

View File

@ -16,9 +16,11 @@ ldc2 --version
# fetch missing packages before timing # fetch missing packages before timing
dub upgrade --missing-only dub upgrade --missing-only
rm -rf .dub bin
start=`date +%s` start=`date +%s`
dub build --build=release --config=client 2>&1 || echo "DCD BUILD FAILED" dub build --build=release --config=client --force 2>&1 || echo "DCD BUILD FAILED"
dub build --build=release --config=server 2>&1 || echo "DCD BUILD FAILED" dub build --build=release --config=server --force 2>&1 || echo "DCD BUILD FAILED"
end=`date +%s` end=`date +%s`
build_time=$( echo "$end - $start" | bc -l ) build_time=$( echo "$end - $start" | bc -l )
@ -32,7 +34,7 @@ echo "STAT:rough build time=${build_time}s"
echo "STAT:" echo "STAT:"
# now rebuild server with -profile=gc # now rebuild server with -profile=gc
dub build --build=profile-gc --config=server 2>&1 || echo "DCD BUILD FAILED" dub build --build=profile-gc --config=server --force 2>&1 || echo "DCD BUILD FAILED"
cd tests cd tests
./run_tests.sh --time-server ./run_tests.sh --time-server