#! /bin/bash
# Last edited on 2008-07-18 18:37:17 by stolfi

# To be included by scripts that fetch files.
# Defines a shell function 'wg {FILE}' that 
# fetches {FILE} from the WWW directory 
# ${rdir} and saves it to local directory ${odir}.
# The {FILE} may contain '/'; the function will 
# create the necessary sub-directories.

# Usage:
#   rdir='http://www...foo'  # Remote directory (without final '/')
#   odir='mycopy/today'      # Local directory (without final '/')
#   wg file1.tex             
#   wg figures/fig1.eps

function wg() {
  file="$1"; shift # file name (without initial '/')
  file="/${file}";  # add initial '/' to ${file}
  subd="${file%/*}" # subdirectory (with initial '/') or empty
  mkdir -p "${odir}${subd}"
  echo "fetching ${odir}${file} ..."
  wget -nv "${rdir}${file}" -O "${odir}${file}"
  ls -l "${odir}${file}"
}