diff -r 5be639c601b2 -r 63249c1c544a lib/Tools/make
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/make	Wed Dec 18 12:47:28 1996 +0100
@@ -0,0 +1,31 @@
+#!/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 "$@"