1.1 --- a/src/Pure/build	Thu Jul 26 12:32:25 2012 +0200
     1.2 +++ b/src/Pure/build	Thu Jul 26 12:59:09 2012 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  function usage()
     1.5  {
     1.6    echo
     1.7 -  echo "Usage: $PRG TARGET OUTPUT"
     1.8 +  echo "Usage: $PRG TARGET [OUTPUT]"
     1.9    echo
    1.10    exit 1
    1.11  }
    1.12 @@ -30,7 +30,10 @@
    1.13  
    1.14  # args
    1.15  
    1.16 -if [ "$#" -eq 2 ]; then
    1.17 +if [ "$#" -eq 1 ]; then
    1.18 +  TARGET="$1"; shift
    1.19 +  OUTPUT=""; shift
    1.20 +elif [ "$#" -eq 2 ]; then
    1.21    TARGET="$1"; shift
    1.22    OUTPUT="$1"; shift
    1.23  else