also generate minidot.tex when running ../bin/tex.sh

TiarkRompf · Oct 17, 2013 · c5225a0 · c5225a0
1 parent b7343e4
commit c5225a0
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/bin/tex.sh b/bin/tex.sh
@@ -13,3 +13,4 @@ command -v $bin >/dev/null 2>&1 || { echo >&2 "twelf-server not found. aborting.
 echo -e "set chatter 0\nloadFile ../dev/dot.elf\nPrint.sgn" | $bin | awk '!/^%%/' | tail -n +2 >dot.txt
 ../bin/twelf2tex.py dot.txt >dot_auto.tex
 pdflatex twelf.tex
+pdflatex minidot.tex