| changeset 2916 | d761a62da697 |
| parent 2332 | ae592411c199 |
| child 2936 | bd33e7aae062 |
| 2915:4d2d409fe2ea | 2916:d761a62da697 |
|---|---|
43 [ -f $DIR/Contents ] && cat $DIR/Contents |
43 [ -f $DIR/Contents ] && cat $DIR/Contents |
44 done |
44 done |
45 else |
45 else |
46 for DIR in $ISABELLE_DOCS |
46 for DIR in $ISABELLE_DOCS |
47 do |
47 do |
48 [ -f $DIR/$DOC.dvi ] && exec $DVI_VIEWER $DIR/$DOC.dvi |
48 [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi } |
49 done |
49 done |
50 fail "Unknown Isabelle document: $DOC" |
50 fail "Unknown Isabelle document: $DOC" |
51 fi |
51 fi |