changeset 28500 | 4b79e5d3d0aa |
parent 15717 | 541e50adfc73 |
child 28650 | a7ba12e0d3b7 |
--- a/lib/Tools/doc Sat Oct 04 16:05:08 2008 +0200 +++ b/lib/Tools/doc Sat Oct 04 16:05:09 2008 +0200 @@ -53,7 +53,7 @@ [ -d "$DIR" ] || fail "Bad document directory: $DIR" for FMT in "$ISABELLE_DOC_FORMAT" dvi do - [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISATOOL" display "$DOC.$FMT"; } + [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISABELLE_TOOL" display "$DOC.$FMT"; } done done IFS="$ORIG_IFS"