From 334b6dd70f0e0f7fe98c429147f1e82f8d0f93a5 Mon Sep 17 00:00:00 2001
From: Phuntsok Drak-pa <phundrak@phundrak.fr>
Date: Wed, 23 May 2018 18:16:33 +0200
Subject: [PATCH] minor update for cleaning script

---
 clean.sh | 12 +-----------
 1 file changed, 1 insertion(+), 11 deletions(-)

diff --git a/clean.sh b/clean.sh
index 7631621..9370c31 100755
--- a/clean.sh
+++ b/clean.sh
@@ -6,17 +6,7 @@ else
     project_root=$1
 fi
 
-rm -rf *~
-rm -rf auto
-rm -rf _minted*
-rm -rf *.tex
-rm -rf *.aux
-rm -rf *.log
-rm -rf *.toc
-rm -rf *.out
-rm -rf index.pdf
-rm -rf headers.pdf
-rm -rf headers.html
+rm -rf *~ auto _minted* *.tex *.aux *.log *.toc *.out index.pdf headers.pdf headers.html
 for filename in *; do
     if [[ -d $filename ]]; then
         cd $filename