#!/bin/sh # Steven Armstrong # Nico Schottelius # set -e DIR="$1" [ -z "${DIR}" ] && DIR="${PWD}" DIR="${DIR%/}" if ! [ -d "${DIR}" ]; then echo "cannot access ${DIR}: No such file or directory" >&2 exit 1 fi cd "${DIR}" rm -f *.aux *.nav *.out *.toc *.snm *.log *.vrb