lib/Tools/doc
changeset 52427 9d1cc9a22177
parent 32390 468eff174a77
child 52444 2cfe6656d6d6
     1.1 --- a/lib/Tools/doc	Sun Jun 23 18:11:38 2013 +0200
     1.2 +++ b/lib/Tools/doc	Sun Jun 23 20:12:01 2013 +0200
     1.3 @@ -39,18 +39,18 @@
     1.4  if [ -z "$DOC" ]; then
     1.5    for DIR in "${DOCS[@]}"
     1.6    do
     1.7 -    [ -d "$DIR" ] || fail "Bad document directory: $DIR"
     1.8 -    [ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents"
     1.9 +    [ -d "$DIR" ] || fail "Bad documentation directory: \"$DIR\""
    1.10 +    [ -f "$DIR/Contents" ] && cat "$DIR/Contents"
    1.11    done
    1.12  else
    1.13    for DIR in "${DOCS[@]}"
    1.14    do
    1.15 -    [ -d "$DIR" ] || fail "Bad document directory: $DIR"
    1.16 +    [ -d "$DIR" ] || fail "Bad documentation directory: \"$DIR\""
    1.17      for FMT in "$ISABELLE_DOC_FORMAT" dvi
    1.18      do
    1.19        [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISABELLE_TOOL" display "$DOC.$FMT"; }
    1.20      done
    1.21    done
    1.22 -  fail "Unknown Isabelle document: $DOC"  
    1.23 +  fail "Missing Isabelle documentation: \"$DOC\""
    1.24  fi
    1.25