Minor clean-up
This commit is contained in:
parent
3dd3652999
commit
7a3cef12b9
@ -28,12 +28,12 @@ pushd "$dir"
|
|||||||
git config user.name "Potassco Bot"
|
git config user.name "Potassco Bot"
|
||||||
git config user.email "bot@potassco.org"
|
git config user.email "bot@potassco.org"
|
||||||
|
|
||||||
echo "start of benchmark output of job $JOB_KEY" > test-output
|
echo "start of benchmark output of job $JOB_KEY" > output
|
||||||
sleep "$TIME"
|
sleep "$TIME"
|
||||||
echo "collected $FRUIT"
|
echo "collected $FRUIT"
|
||||||
start_time=$(date +%s%N)
|
start_time=$(date +%s%N)
|
||||||
echo "end of benchmark output of job $JOB_KEY" >> test-output
|
echo "end of benchmark output of job $JOB_KEY" >> output
|
||||||
git add test-output
|
git add output
|
||||||
git commit -m "Add results of job $JOB_KEY"
|
git commit -m "Add results of job $JOB_KEY"
|
||||||
git push
|
git push
|
||||||
end_time=$(date +%s%N)
|
end_time=$(date +%s%N)
|
||||||
|
Loading…
Reference in New Issue
Block a user