equal
deleted
inserted
replaced
20 NAME="$1"; shift |
20 NAME="$1"; shift |
21 else |
21 else |
22 usage |
22 usage |
23 fi |
23 fi |
24 |
24 |
25 "$ISATOOL" mkdir -b -q "$NAME" |
25 "$ISABELLE_TOOL" mkdir -b -q "$NAME" |
26 (cd document; "$ISATOOL" latex -o sty) |
26 ( cd document; "$ISABELLE_TOOL" latex -o sty; ) |
27 |
|