1.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Wed Jul 06 23:11:59 2011 +0200
     1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Jul 07 13:48:30 2011 +0200
     1.3 @@ -202,9 +202,7 @@
     1.4  
     1.5  if [ "$OUTDATED" = true ]
     1.6  then
     1.7 -  echo "###"
     1.8    echo "### Building Isabelle/jEdit ..."
     1.9 -  echo "###"
    1.10  
    1.11    [ "${#UPDATED[@]}" -gt 0 ] && {
    1.12      echo "Changed files:"