src/Pure/Makefile
changeset 2117 292df12bace5
parent 2094 2061df98aab5
child 2195 e8271379ba4b
     1.1 --- a/src/Pure/Makefile	Mon Oct 21 09:51:18 1996 +0200
     1.2 +++ b/src/Pure/Makefile	Mon Oct 21 11:18:34 1996 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4  
     1.5  #Uses cp rather than make_database because Poly/ML allows only 3 levels
     1.6  $(BIN)/Pure:   $(FILES)	 $(SYNTAX_FILES)  $(THY_FILES)	$(ML_DBASE)
     1.7 -	case "$(COMP)" in \
     1.8 +	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
     1.9  	poly*)	echo database=$${ML_DBASE:?'No Poly/ML database specified'};\
    1.10  		cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
    1.11  		echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' \
    1.12 @@ -50,7 +50,7 @@
    1.13  		fi;\
    1.14  		echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1;				     xML"$(BIN)/Pure" banner;' | $(COMP);;\
    1.15  	*)	echo Bad value for ISABELLECOMP: \
    1.16 -			$(COMP) is not poly or sml;;\
    1.17 +			\"$(COMP)\" is not poly or sml;;\
    1.18  	esac
    1.19  
    1.20