Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit 425c385c authored by MARCHE Claude's avatar MARCHE Claude
Browse files

make the nightly bench script identical for each git branch

parent 832be2e5
......@@ -11,14 +11,21 @@ case "$1" in
exit 2
esac
REPORTDIR=$PWD/../why3-reports
GITBRANCH=`git rev-parse --abbrev-ref HEAD`
REPORTDIR=$PWD/../why3-reports-$GITBRANCH
if ! test -e "$REPORTDIR"; then
echo "directory '$REPORTDIR' for reports does not exist, aborting."
exit 2
fi
OUT=$REPORTDIR/nightly-bench.out
PREVIOUS=$REPORTDIR/nightly-bench.previous
DIFF=$REPORTDIR/nightly-bench.diff
REPORT=$REPORTDIR/nightly-bench.report
DATE=`date --utc +%Y-%m-%d`
SUBJECT="Why3 nightly bench:"
SUBJECT="Why3 [$GITBRANCH] bench : "
notify() {
if test "$REPORTBYMAIL" == "no"; then
......@@ -32,6 +39,8 @@ notify() {
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
# configuration
autoconf
......@@ -127,7 +136,7 @@ if test "$?" != "0" ; then
echo "Proof replay failed" >> $REPORT
else
SUBJECT="$SUBJECT successful"
echo " !!! REPLAY SUCCEEDED !!! YAHOOOO !!! " >> $REPORT
echo "REPLAY SUCCEEDED" >> $REPORT
fi
# store the state for this day
......
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