|
|
|
@ -7,10 +7,6 @@
|
|
|
|
|
|
|
|
|
|
tmp_dir=/home/pluehne/tmp |
|
|
|
|
|
|
|
|
|
echo "job ID: $JOB_ID" |
|
|
|
|
echo "job key: $JOB_KEY" |
|
|
|
|
echo "job result repository URL: $JOB_RESULT_REPOSITORY_URL" |
|
|
|
|
|
|
|
|
|
mkdir -p "$tmp_dir" |
|
|
|
|
dir="$tmp_dir"/"job-$JOB_ID" |
|
|
|
|
|
|
|
|
@ -29,15 +25,14 @@ pushd "$dir"
|
|
|
|
|
git config user.email "bot@potassco.org" |
|
|
|
|
|
|
|
|
|
echo "start of benchmark output of job $JOB_KEY" > output |
|
|
|
|
|
|
|
|
|
sleep "$TIME" |
|
|
|
|
echo "collected $FRUIT" >> output |
|
|
|
|
start_time=$(date +%s%N) |
|
|
|
|
|
|
|
|
|
echo "end of benchmark output of job $JOB_KEY" >> output |
|
|
|
|
|
|
|
|
|
git add output |
|
|
|
|
git commit -m "Add results of job $JOB_KEY" |
|
|
|
|
git push |
|
|
|
|
end_time=$(date +%s%N) |
|
|
|
|
popd |
|
|
|
|
|
|
|
|
|
echo $(expr "$end_time" - "$start_time") >> "$tmp_dir"/overhead |
|
|
|
|
popd |