#! /bin/csh -fe
# Last edited on 2003-10-12 15:30:14 by stolfi

# Applies a 'sed' script to a set of files
# Usage: sed-files -f <script file> <file>...

set path = ( /usr/bin /bin ${STOLFIHOME}/bin /usr/ucb /usr/bsd )

# GNU "sed" seems to be more robust than standard "sed"
if ( -x /usr/bin/sed ) then
  set sed = "/usr/bin/sed"
else
  set sed = "/bin/sed"
endif

set diffopt = ( )
if ("$1" == "-h" ) then
  set diffopt = ( "$1" )
  shift
endif

if ("$1" != '-f') then
  echo Usage: 'sed-files -f script-file file ...'
  exit(1)
endif
if ( ! (-f "$2") ) then
  echo "$2 is not a file\!"
  exit(1)
endif
${STOLFIHOME}/bin/filter-files ${diffopt} "${sed} -f $2" $argv[3-]
