diff --git a/autocompile.sh b/autocompile.sh index 5d609350044402a2797a3e13bb104feb6d5b0c24..df25901fc362ba094e8a253a0f936dea71611357 100755 --- a/autocompile.sh +++ b/autocompile.sh @@ -1,5 +1,10 @@ #!/bin/bash -if [ ! -z $1 ]; then +if [ $1 = clean ]; then + rm *aux *log main.{i,g}* *toc + exit 0 +fi + +if [ $1 = conf ]; then git subtree -P config pull ../config master && \ git subtree -P config push ../config core fi