view workers/bin/_doFetch.sh @ 43:c2b72d29a3ee

update to use _timedWhich.py
author Henry S. Thompson <ht@markup.co.uk>
date Fri, 30 Nov 2018 18:37:40 +0000
parents 4c117ee8ed75
children
line wrap: on
line source

#!/bin/bash
id=$1
home=$2
pause=$3
log=$4
shift 4
echo \#.$id fetch $(echo "$@" | wc -w) >> $log
until ssh $home "xargs gzip -c" "$@"  | gunzip -c > /var/data/d${id}.x 
 do
  echo retrying 1>&2
  sleep $pause
done
echo \# # put a group mark in for timing purposes further down the line
cat /var/data/d${id}.x | tee >(echo \#.$id fetched $(wc -l) >> $log)