src/Pure/Makefile
changeset 2235 866dbb04816c
parent 2195 e8271379ba4b
child 2692 484ec6ca0c50
     1.1 --- a/src/Pure/Makefile	Tue Nov 26 17:49:25 1996 +0100
     1.2 +++ b/src/Pure/Makefile	Wed Nov 27 10:31:05 1996 +0100
     1.3 @@ -21,7 +21,8 @@
     1.4  
     1.5  BIN = $(ISABELLEBIN)
     1.6  COMP = $(ISABELLECOMP)
     1.7 -FILES =	POLY.ML NJ.ML ROOT.ML library.ML term.ML symtab.ML type.ML sign.ML\
     1.8 +FILES =	POLY.ML NJ.ML NJ093.ML NJ1xx.ML ROOT.ML basis.ML library.ML\
     1.9 +	term.ML symtab.ML type.ML sign.ML\
    1.10  	sequence.ML envir.ML pattern.ML unify.ML logic.ML theory.ML thm.ML\
    1.11  	net.ML display.ML deriv.ML drule.ML tctical.ML search.ML tactic.ML\
    1.12  	goals.ML axclass.ML install_pp.ML\
    1.13 @@ -37,7 +38,7 @@
    1.14  
    1.15  #Uses cp rather than make_database because Poly/ML allows only 3 levels
    1.16  $(BIN)/Pure:   $(FILES)	 $(SYNTAX_FILES)  $(THY_FILES)	$(ML_DBASE)
    1.17 -	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
    1.18 +	@case `basename "$(COMP)"` in \
    1.19  	poly*)	echo database=$${ML_DBASE:?'No Poly/ML database specified'};\
    1.20  		cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
    1.21  		echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' \
    1.22 @@ -49,8 +50,8 @@
    1.23  			exit 1; \
    1.24  		fi;\
    1.25  		echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1;				     xML"$(BIN)/Pure" banner;' | $(COMP);;\
    1.26 -	*)	echo Bad value for ISABELLECOMP: \
    1.27 -			\"$(COMP)\" is not poly or sml;;\
    1.28 +	*)	echo Bad value for ISABELLECOMP: $(COMP); \
    1.29 +		echo "   " \"`basename "$(COMP)"`\" is not poly or sml;;\
    1.30  	esac
    1.31  
    1.32