src/Pure/build
changeset 49526 37999ee01156
parent 49462 ef600ce4559c
child 49677 b171bcd5dd86
equal deleted inserted replaced
49525:8f3069015441 49526:37999ee01156
    10 ## diagnostics
    10 ## diagnostics
    11 
    11 
    12 function usage()
    12 function usage()
    13 {
    13 {
    14   echo
    14   echo
    15   echo "Usage: $PRG TARGET OUTPUT"
    15   echo "Usage: $PRG TARGET [OUTPUT]"
    16   echo
    16   echo
    17   exit 1
    17   exit 1
    18 }
    18 }
    19 
    19 
    20 function fail()
    20 function fail()
    28 
    28 
    29 ## process command line
    29 ## process command line
    30 
    30 
    31 # args
    31 # args
    32 
    32 
    33 if [ "$#" -eq 2 ]; then
    33 if [ "$#" -eq 1 ]; then
       
    34   TARGET="$1"; shift
       
    35   OUTPUT=""; shift
       
    36 elif [ "$#" -eq 2 ]; then
    34   TARGET="$1"; shift
    37   TARGET="$1"; shift
    35   OUTPUT="$1"; shift
    38   OUTPUT="$1"; shift
    36 else
    39 else
    37   usage
    40   usage
    38 fi
    41 fi