Commit 255164f9 authored by MARCHE Claude's avatar MARCHE Claude

put proper email subject when bench is not run

parent b0011383
...@@ -44,6 +44,7 @@ NEWCOMMITHASH=$(git rev-parse HEAD) ...@@ -44,6 +44,7 @@ NEWCOMMITHASH=$(git rev-parse HEAD)
if test $LASTCOMMITHASH = $NEWCOMMITHASH; then if test $LASTCOMMITHASH = $NEWCOMMITHASH; then
echo "Not running nightly bench: last commit is the same as for previous run" > $REPORT echo "Not running nightly bench: last commit is the same as for previous run" > $REPORT
SUBJECT="$SUBJECT not run (no new commit)"
else else
echo "== Why3 bench on $DATE ==" > $REPORT echo "== Why3 bench on $DATE ==" > $REPORT
echo "Starting time (UTC): "`date --utc +%H:%M` >> $REPORT echo "Starting time (UTC): "`date --utc +%H:%M` >> $REPORT
......
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