mirroring log entries need the *date* also in the timestamp!

(Not sure how I missed this earlier, but if you can't upgrade yet, a
mitigation is to note the job number that gets printed on your terminal
when a mirror push starts, and look a log file entries beginning with
that number.)
This commit is contained in:
Sitaram Chamarty 2011-10-04 19:03:39 +05:30
parent de9ece4735
commit eabbffb564

View file

@ -70,14 +70,14 @@ exec >>$logfile 2>&1 </dev/null
# double fork, no zombies
(
(
echo `date +%T` $repo '===>'
echo `date +%F.%T` $repo '===>'
for s in $slaves
do
[ "$s" = "$hn" ] && continue # skip ourselves
git push --mirror $s:$repo || echo ==== WARNING: RC=$? from git push --mirror $s:$repo ====
done 2>&1 | sed -e "s/^/ /"
echo `date +%T` '===>' $slaves
echo `date +%F.%T` '===>' $slaves
echo
) 2>&1 | sed -e "s/^/$job_id:/" & # background the whole thing
)