lib/Tools/make
author wenzelm
Wed, 18 Dec 1996 12:47:28 +0100
changeset 2437 63249c1c544a
child 2501 632e126852fc
permissions -rwxr-xr-x
Isabelle make utility;

#!/bin/bash -norc
#
# $Id$
#
# DESCRIPTION: Isabelle make utility


PRG=$(basename $0)

function usage()
{
  echo
  echo "Usage: $PRG [ARGS ...]"
  echo
  echo "  Compiles logic in current directory using IsaMakefile."
  echo "  ARGS are directly passed to the system make program."
  echo
  exit 1
}


## main

[ "$1" = "-?" ] && usage


. $ISABELLE_HOME/lib/scripts/getplatform

export ISABELLE_OUTPUT_DIR="$ISABELLE_OUTPUT/$ML_SYSTEM-$PLATFORM"

exec make -f IsaMakefile "$@"