#! /bin/bash
# Last edited on 2014-08-29 07:51:52 by stolfilocal
# To be source'd in sh 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:
export ext=".${name##*.}"
if [[ "${ext}" == "." ]]; then
  export ext=""
elif [[ ( "${ext}" == ".tex" ) || ( "${ext}" == ".iso" ) ]]; then
  export name="${name%.*}"
else
  export ext=""
fi

if [[ "/${ext}" == "/" ]]; then
  # Choose an extension by checking for file existence:
  if [[ -s "${name}.tex" ]]; then
    export ext=".tex"
  elif [[ -s "${name}.iso" ]]; then
    export ext=".iso";
  elif [[ -r "${name}" ]]; then
    export ext="${ext}"
  else
    echo "${name}" not found; exit 1
  fi
else
  # Ensure file exists:
  if [[ ! ( -s "${name}${ext}" ) ]]; then
    echo "${name}${ext} not found" 1>&2; exit 1
  fi
fi