diff -r 1291a8f2ccb1 -r 541e50adfc73 lib/Tools/doc
--- a/lib/Tools/doc	Wed Apr 13 18:47:53 2005 +0200
+++ b/lib/Tools/doc	Wed Apr 13 18:48:05 2005 +0200
@@ -59,3 +59,4 @@
   IFS="$ORIG_IFS"
   fail "Unknown Isabelle document: $DOC"  
 fi
+