equal
deleted
inserted
replaced
51 do |
51 do |
52 IFS="$ORIG_IFS" |
52 IFS="$ORIG_IFS" |
53 [ -d "$DIR" ] || fail "Bad document directory: $DIR" |
53 [ -d "$DIR" ] || fail "Bad document directory: $DIR" |
54 for FMT in "$ISABELLE_DOC_FORMAT" dvi |
54 for FMT in "$ISABELLE_DOC_FORMAT" dvi |
55 do |
55 do |
56 [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISATOOL" display "$DOC.$FMT"; } |
56 [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISABELLE_TOOL" display "$DOC.$FMT"; } |
57 done |
57 done |
58 done |
58 done |
59 IFS="$ORIG_IFS" |
59 IFS="$ORIG_IFS" |
60 fail "Unknown Isabelle document: $DOC" |
60 fail "Unknown Isabelle document: $DOC" |
61 fi |
61 fi |