--- a/src/Pure/mk Mon Oct 06 09:26:00 1997 +0200
+++ b/src/Pure/mk Mon Oct 06 18:20:15 1997 +0200
@@ -9,6 +9,18 @@
## diagnostics
+function usage()
+{
+ echo
+ echo "Usage: $PRG [OPTIONS]"
+ echo
+ echo " Make Pure Isabelle."
+ echo
+ echo " -r just prepare RAW image"
+ echo
+ exit 1
+}
+
function fail()
{
echo "$1" >&2
@@ -16,6 +28,32 @@
}
+## process command line
+
+# options
+
+RAW=""
+
+while getopts "r" OPT
+do
+ case "$OPT" in
+ r)
+ RAW=true
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ $# -ne 0 ] && usage
+
+
## main
ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
@@ -27,7 +65,14 @@
[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
-$ISABELLE \
- -e "val ml_system = \"$ML_SYSTEM\";" \
- -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
- -q -w RAW_ML_SYSTEM Pure
+if [ -z "$RAW" ]; then
+ $ISABELLE \
+ -e "val ml_system = \"$ML_SYSTEM\";" \
+ -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
+ -q -w RAW_ML_SYSTEM Pure
+else
+ $ISABELLE \
+ -e "val ml_system = \"$ML_SYSTEM\";" \
+ -e "use\"$COMPAT\";" \
+ -q -w RAW_ML_SYSTEM RAW
+fi