src/Pure/Makefile
changeset 408 93e2b7d5bcc4
parent 407 8039ac1065f7
child 415 e5470bf81350
     1.1 --- a/src/Pure/Makefile	Wed Jun 01 08:28:12 1994 +0200
     1.2 +++ b/src/Pure/Makefile	Wed Jun 01 13:11:40 1994 +0200
     1.3 @@ -38,13 +38,14 @@
     1.4  		cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
     1.5  		echo 'PolyML.use"POLY";use"ROOT";' | $(COMP) $(BIN)/Pure;;\
     1.6  	sml*)	if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\
     1.7 -           	then echo Bad value for ISABELLEBIN : \
     1.8 +           	then echo Bad value for ISABELLEBIN: \
     1.9                  	$(BIN) is not a writable directory; \
    1.10                  	exit 1; \
    1.11             	fi;\
    1.12  		echo 'use"NJ.ML"; use"ROOT.ML"; xML"$(BIN)/Pure" banner;'\
    1.13  			  | $(COMP);;\
    1.14 -	*)	echo Bad value for ISABELLECOMP;;\
    1.15 +	*)	echo Bad value for ISABELLECOMP: \
    1.16 +                	$(COMP) is not poly or sml;;\
    1.17  	esac
    1.18  
    1.19  .PRECIOUS:  $(BIN)/Pure