# HG changeset patch
# User lcp
# Date 795261238 -3600
# Node ID d3f734f661417d66f2d59cf4b6d383348ed2ca20
# Parent  17d7fad9c9a22bbb16b2950e71f4b0c19cf1c7db
Now the "use" call has an exception handler, for prompt failure
if errors are detected.

diff -r 17d7fad9c9a2 -r d3f734f66141 src/Pure/Makefile
--- a/src/Pure/Makefile	Wed Mar 15 10:34:47 1995 +0100
+++ b/src/Pure/Makefile	Wed Mar 15 10:53:58 1995 +0100
@@ -37,13 +37,13 @@
 	case "$(COMP)" in \
 	poly*)	echo database=$${ML_DBASE:?'No Poly/ML database specified'};\
 		cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
-		echo 'PolyML.use"POLY";use"ROOT";' | $(COMP) $(BIN)/Pure;;\
+		echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' | $(COMP) $(BIN)/Pure;;\
 	sml*)	if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\
            	then echo Bad value for ISABELLEBIN: \
                 	$(BIN) is not a writable directory; \
                 	exit 1; \
            	fi;\
-		echo 'use"NJ.ML"; use"ROOT.ML"; xML"$(BIN)/Pure" banner;'\
+		echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1; xML"$(BIN)/Pure" banner;'\
 			  | $(COMP);;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml;;\