src/Pure/build

--- a/src/Pure/build	Thu Jul 26 12:32:25 2012 +0200
+++ b/src/Pure/build	Thu Jul 26 12:59:09 2012 +0200
@@ -12,7 +12,7 @@
 function usage()
 {
   echo
-  echo "Usage: $PRG TARGET OUTPUT"
+  echo "Usage: $PRG TARGET [OUTPUT]"
   echo
   exit 1
 }
@@ -30,7 +30,10 @@
 
 # args
 
-if [ "$#" -eq 2 ]; then
+if [ "$#" -eq 1 ]; then
+  TARGET="$1"; shift
+  OUTPUT=""; shift
+elif [ "$#" -eq 2 ]; then
   TARGET="$1"; shift
   OUTPUT="$1"; shift
 else