equal
deleted
inserted
replaced
37 DOCS=$(echo $ISABELLE_DOCS | tr : " ") |
37 DOCS=$(echo $ISABELLE_DOCS | tr : " ") |
38 |
38 |
39 if [ -z "$DOC" ]; then |
39 if [ -z "$DOC" ]; then |
40 for DIR in $DOCS |
40 for DIR in $DOCS |
41 do |
41 do |
42 [ -f $DIR/Contents ] && cat $DIR/Contents |
42 [ -f $DIR/Contents ] && grep -v "^>>" $DIR/Contents |
43 done |
43 done |
44 else |
44 else |
45 for DIR in $DOCS |
45 for DIR in $DOCS |
46 do |
46 do |
47 [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi; } |
47 [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi; } |