From c5225a0788f03f8e05f6f1731b6ddeb273057d2c Mon Sep 17 00:00:00 2001
From: Nada Amin <namin@alum.mit.edu>
Date: Thu, 17 Oct 2013 08:30:32 +0200
Subject: [PATCH] also generate minidot.tex when running ../bin/tex.sh

---
 bin/tex.sh | 1 +
 1 file changed, 1 insertion(+)

diff --git a/bin/tex.sh b/bin/tex.sh
index e63a95e4..96b21b8c 100755
--- 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