#!/bin/sh # Steven Armstrong # Nico Schottelius # 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 rm "${DIR}"/*.{aux,nav,out,toc,snm,log,vrb}