Admin/bash_process/build
author wenzelm
Sat Jun 02 22:40:03 2018 +0200 (17 months ago)
changeset 68358 e761afd35baa
parent 66691 a8703e8ee1d3
permissions -rwxr-xr-x
tuned proofs;
     1 #!/usr/bin/env bash
     2 #
     3 # Multi-platform build script
     4 
     5 THIS="$(cd "$(dirname "$0")"; pwd)"
     6 PRG="$(basename "$0")"
     7 
     8 
     9 # diagnostics
    10 
    11 function usage()
    12 {
    13   echo
    14   echo "Usage: $PRG TARGET"
    15   echo
    16   exit 1
    17 }
    18 
    19 function fail()
    20 {
    21   echo "$1" >&2
    22   exit 2
    23 }
    24 
    25 
    26 # command line args
    27 
    28 [ "$#" -eq 0 ] && usage
    29 TARGET="$1"; shift
    30 
    31 [ "$#" -eq 0 ] || usage
    32 
    33 
    34 # main
    35 
    36 mkdir -p "$TARGET"
    37 
    38 case "$TARGET" in
    39   x86_64-linux | x86_64-darwin)
    40     cc -Wall -m64 bash_process.c -o "$TARGET/bash_process"
    41     ;;
    42   x86-linux | x86-darwin)
    43     cc -Wall -m32 bash_process.c -o "$TARGET/bash_process"
    44     ;;
    45   x86_64-cygwin | x86-cygwin)
    46     cc -Wall bash_process.c -o "$TARGET/bash_process.exe"
    47     ;;
    48   *)
    49     cc -Wall bash_process.c -o "$TARGET/bash_process"
    50     ;;
    51 esac