# HG changeset patch
# User wenzelm
# Date 861974338 -7200
# Node ID 200565f7592add41c4da5b7cf9a8e6d7b3358675
# Parent  5da4afa207adec65b9f22b873a2a32b81f299428
removed -c option;

diff -r 5da4afa207ad -r 200565f7592a src/Pure/mk
--- a/src/Pure/mk	Fri Apr 25 15:10:52 1997 +0200
+++ b/src/Pure/mk	Fri Apr 25 15:18:58 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #
@@ -19,7 +19,8 @@
 ## main
 
 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
-[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Probably not run via 'isatool make'?."
+[ -z "$ML_SYSTEM" ] && \
+  fail "Missing ML system settings! Probably not run via 'isatool make'?."
 
 COMPAT=""
 [ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
@@ -29,6 +30,6 @@
 $ISABELLE \
   -e "val ml_system = \"$ML_SYSTEM\";" \
   -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
-  -cq RAW_ML_SYSTEM Pure
+  -q RAW_ML_SYSTEM Pure
 
 chmod -w $ISABELLE_OUTPUT_DIR/Pure