lib/Tools/doc
changeset 52427 9d1cc9a22177
parent 32390 468eff174a77
child 52444 2cfe6656d6d6
--- a/lib/Tools/doc	Sun Jun 23 18:11:38 2013 +0200
+++ b/lib/Tools/doc	Sun Jun 23 20:12:01 2013 +0200
@@ -39,18 +39,18 @@
 if [ -z "$DOC" ]; then
   for DIR in "${DOCS[@]}"
   do
-    [ -d "$DIR" ] || fail "Bad document directory: $DIR"
-    [ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents"
+    [ -d "$DIR" ] || fail "Bad documentation directory: \"$DIR\""
+    [ -f "$DIR/Contents" ] && cat "$DIR/Contents"
   done
 else
   for DIR in "${DOCS[@]}"
   do
-    [ -d "$DIR" ] || fail "Bad document directory: $DIR"
+    [ -d "$DIR" ] || fail "Bad documentation directory: \"$DIR\""
     for FMT in "$ISABELLE_DOC_FORMAT" dvi
     do
       [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISABELLE_TOOL" display "$DOC.$FMT"; }
     done
   done
-  fail "Unknown Isabelle document: $DOC"  
+  fail "Missing Isabelle documentation: \"$DOC\""
 fi