Now the "use" call has an exception handler, for prompt failure
authorlcp
Wed, 15 Mar 1995 10:53:58 +0100
changeset 954d3f734f66141
parent 953 17d7fad9c9a2
child 955 aa0c5f9daf5b
Now the "use" call has an exception handler, for prompt failure
if errors are detected.
src/Pure/Makefile
     1.1 --- a/src/Pure/Makefile	Wed Mar 15 10:34:47 1995 +0100
     1.2 +++ b/src/Pure/Makefile	Wed Mar 15 10:53:58 1995 +0100
     1.3 @@ -37,13 +37,13 @@
     1.4  	case "$(COMP)" in \
     1.5  	poly*)	echo database=$${ML_DBASE:?'No Poly/ML database specified'};\
     1.6  		cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
     1.7 -		echo 'PolyML.use"POLY";use"ROOT";' | $(COMP) $(BIN)/Pure;;\
     1.8 +		echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' | $(COMP) $(BIN)/Pure;;\
     1.9  	sml*)	if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\
    1.10             	then echo Bad value for ISABELLEBIN: \
    1.11                  	$(BIN) is not a writable directory; \
    1.12                  	exit 1; \
    1.13             	fi;\
    1.14 -		echo 'use"NJ.ML"; use"ROOT.ML"; xML"$(BIN)/Pure" banner;'\
    1.15 +		echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1; xML"$(BIN)/Pure" banner;'\
    1.16  			  | $(COMP);;\
    1.17  	*)	echo Bad value for ISABELLECOMP: \
    1.18                  	$(COMP) is not poly or sml;;\