Commit b0011383 authored by MARCHE Claude's avatar MARCHE Claude

nightly bench: do not run if there was no commit since the last run

# Conflicts:
#	misc/nightly-bench.sh
parent d885e9d0
......@@ -25,6 +25,8 @@ if ! test -e "$REPORTDIR"; then
touch "$PREVIOUS"
fi
LASTCOMMIT=$REPORTDIR/lastcommit
DATE=`date --utc +%Y-%m-%d`
SUBJECT="Why3 [$GITBRANCH] bench : "
......@@ -37,11 +39,16 @@ notify() {
exit 0
}
LASTCOMMITHASH=$(cat $LASTCOMMIT 2>/dev/null || echo 'none')
NEWCOMMITHASH=$(git rev-parse HEAD)
if test $LASTCOMMITHASH = $NEWCOMMITHASH; then
echo "Not running nightly bench: last commit is the same as for previous run" > $REPORT
else
echo "== Why3 bench on $DATE ==" > $REPORT
echo "Starting time (UTC): "`date --utc +%H:%M` >> $REPORT
echo "Current branch: "$GITBRANCH >> $REPORT
echo "Current commit: "`git rev-parse HEAD` >> $REPORT
echo "Current commit: "$NEWCOMMITHASH >> $REPORT
# configuration
autoconf
......@@ -153,5 +160,9 @@ echo "-------------- Full current state --------------" >> $REPORT
echo "" >> $REPORT
cat $OUT >> $REPORT
echo $NEWCOMMITHASH > $LASTCOMMIT
fi # end of test if LASTCOMMITHASH = NEWCOMMITHASH
# final notification after the replay
notify
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment