# HG changeset patch
# User wenzelm
# Date 850143941 -3600
# Node ID 2d5551c8dec054e28fd110102eaeed4308967133
# Parent  1871df9900bfcfa80bfbd9210df68b3549c28e0a
mk - build Pure Isabelle.

diff -r 1871df9900bf -r 2d5551c8dec0 src/Pure/mk
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/mk	Mon Dec 09 16:05:41 1996 +0100
@@ -0,0 +1,33 @@
+#!/bin/bash -norc
+#
+# $Id$
+#
+# mk - build Pure Isabelle.
+#
+# Notes:
+#   (1) edit etc/settings approprately
+#   (2) cd here and run ./mk
+#
+
+
+## diagnostics
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## main
+
+ML_SYSTEM=$(isatool getenv ML_SYSTEM)
+ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
+[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to build Isabelle."
+
+COMPAT=""
+[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
+[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
+[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
+
+exec isabelle -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" -cq SYSTEM Pure