Admin/bash_process/build

clarified directory names (e.g. for multi-platform remote execution): avoid being deleted via isabelle.Components.purge;

#!/usr/bin/env bash
#
# Multi-platform build script

unset CDPATH
THIS="$(cd "$(dirname "$0")"; pwd)"
PRG="$(basename "$0")"


# diagnostics

function usage()
{
  echo
  echo "Usage: $PRG PLATFORM"
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


# command line args

[ "$#" -eq 0 ] && usage
PLATFORM="$1"; shift

[ "$#" -eq 0 ] || usage


# main

PLATFORM_DIR="platform_${PLATFORM}"

case "$PLATFORM" in
  arm64-linux)
    mkdir -p "$PLATFORM_DIR"
    cc -Wall bash_process.c -o "$PLATFORM_DIR/bash_process"
    ;;
  x86_64-linux | x86_64-darwin)
    mkdir -p "$PLATFORM_DIR"
    cc -Wall -m64 bash_process.c -o "$PLATFORM_DIR/bash_process"
    ;;
  x86_64-cygwin)
    mkdir -p "$PLATFORM_DIR"
    cc -Wall bash_process.c -o "$PLATFORM_DIR/bash_process.exe"
    ;;
  *)
    fail "Bad target platform: \"$PLATFORM\""
    ;;
esac