--- a/src/Pure/mk Thu Apr 21 15:05:24 2005 +0200 +++ b/src/Pure/mk Thu Apr 21 15:33:30 2005 +0200 @@ -87,9 +87,6 @@ if [ -z "$RAW" ]; then ITEM="Pure" echo "Building $ITEM ..." - - echo "raw is $RAW item is $ITEM isabelle is $ISABELLE" - LOG="$LOGDIR/$ITEM" "$ISABELLE" $COPY \