src/Pure/mk
author wenzelm
Mon, 07 Jul 1997 09:09:21 +0200
changeset 3505 1cb4ea47d967
parent 3118 24dae6222579
child 3774 b1bfd394b60a
permissions -rwxr-xr-x
eliminated chmod -w;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3056
200565f7592a removed -c option;
wenzelm
parents: 2768
diff changeset
     1
#!/bin/bash
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     2
#
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     3
# $Id$
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     4
#
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     5
# mk - build Pure Isabelle.
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     6
#
2432
527b5f1b7520 minor modifications to accomodate IsaMakefile;
wenzelm
parents: 2401
diff changeset
     7
# Assumes to be called via Isabelle make utility (cf. IsaMakefile).
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     8
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
     9
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    10
## diagnostics
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    11
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    12
function fail()
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    13
{
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    14
  echo "$1" >&2
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    15
  exit 2
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    16
}
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    17
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    18
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    19
## main
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    20
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    21
ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
3056
200565f7592a removed -c option;
wenzelm
parents: 2768
diff changeset
    22
[ -z "$ML_SYSTEM" ] && \
200565f7592a removed -c option;
wenzelm
parents: 2768
diff changeset
    23
  fail "Missing ML system settings! Probably not run via 'isatool make'?."
2339
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    24
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    25
COMPAT=""
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    26
[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    27
[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    28
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
2d5551c8dec0 mk - build Pure Isabelle.
wenzelm
parents:
diff changeset
    29
2474
9990f088d7ac minor tuning;
wenzelm
parents: 2432
diff changeset
    30
$ISABELLE \
2401
0293bc1cecfc now passes ML_SYSTEM as ml_system;
wenzelm
parents: 2340
diff changeset
    31
  -e "val ml_system = \"$ML_SYSTEM\";" \
0293bc1cecfc now passes ML_SYSTEM as ml_system;
wenzelm
parents: 2340
diff changeset
    32
  -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
3505
1cb4ea47d967 eliminated chmod -w;
wenzelm
parents: 3118
diff changeset
    33
  -q -w RAW_ML_SYSTEM Pure