From dee061179f58d7dafb5fa9323d6daecd7e981e92 Mon Sep 17 00:00:00 2001 From: Gerasimos Chourdakis Date: Sun, 17 May 2026 18:09:56 +0200 Subject: [PATCH] log.sh: Use explicit format for date --- tools/log.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tools/log.sh b/tools/log.sh index addcaeb7c..c3c95afb5 100644 --- a/tools/log.sh +++ b/tools/log.sh @@ -5,13 +5,13 @@ CASENAME="$(pwd | xargs basename)" LOGFILE="$CASENAME.log" export LOGFILE -STARTDATE="$(date --rfc-email)" +STARTDATE="$(date '+%a, %d %b %Y %H:%M:%S %z')" STARTTIME="$(date +%s)" echo "Started on: $STARTDATE" | tee "$CASENAME.log" 2>&1 close_log() { echo "Started on: $STARTDATE" | tee --append "$LOGFILE" 2>&1 - ENDDATE="$(date --rfc-email)" + ENDDATE="$(date '+%a, %d %b %Y %H:%M:%S %z')" ENDTIME="$(date +%s)" echo "Finished on: $ENDDATE" | tee --append "$LOGFILE" 2>&1 echo "Duration: $((ENDTIME-STARTTIME)) seconds (wall-clock time, including time waiting for participants)" | tee --append "$LOGFILE" 2>&1