20 lines
		
	
	
	
		
			277 B
		
	
	
	
		
			Bash
		
	
	
		
			Executable file
		
	
	
	
	
			
		
		
	
	
			20 lines
		
	
	
	
		
			277 B
		
	
	
	
		
			Bash
		
	
	
		
			Executable file
		
	
	
	
	
#!/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
 |