changeset 28500 | 4b79e5d3d0aa |
parent 24206 | 9572c9374dc6 |
child 28650 | a7ba12e0d3b7 |
--- a/lib/Tools/mkproject Sat Oct 04 16:05:08 2008 +0200 +++ b/lib/Tools/mkproject Sat Oct 04 16:05:09 2008 +0200 @@ -22,6 +22,5 @@ usage fi -"$ISATOOL" mkdir -b -q "$NAME" -(cd document; "$ISATOOL" latex -o sty) - +"$ISABELLE_TOOL" mkdir -b -q "$NAME" +( cd document; "$ISABELLE_TOOL" latex -o sty; )