#! /bin/csh -f
# Last edited on 2003-06-07 13:28:13 by stolfi
# To be source'd in csh scripts

# Parses the $name variable into a job name $name and and extension
# $ext (either empty or ".tex" or ".iso"), checking for file
# existence. Bombs out if the file does not exist.

# If the name has a standard extension, that is it:
if ( ".${name:e}" == "." ) then
  set ext = ""
else if ( ( ".${name:e}" == ".tex" ) || ( ".${name:e}" == ".iso" ) ) then
  set ext = ".${name:e}"
  set name = "${name:r}"
else
  set ext = ""
endif

if ( "/${ext}" == "/" ) then
  # Choose an extension by checking for file existence:
  if ( -r "${name}.tex" ) then
    set ext = ".tex"
  else if ( -r "${name}.iso" ) then
    set ext = ".iso";
  else if ( -r "${name}" ) then
    # OK
  else
    echo "${name}" not found; exit 1
  endif
else
  # Ensure file exists:
  if ( ! ( -r "${name}${ext}" ) ) then
    echo "${name}${ext}" not found; exit 1
  endif
endif
