--- a/src/Pure/Makefile Mon Oct 21 09:51:18 1996 +0200
+++ b/src/Pure/Makefile Mon Oct 21 11:18:34 1996 +0200
@@ -37,7 +37,7 @@
#Uses cp rather than make_database because Poly/ML allows only 3 levels
$(BIN)/Pure: $(FILES) $(SYNTAX_FILES) $(THY_FILES) $(ML_DBASE)
- case "$(COMP)" in \
+ @case `expr "//$(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" handle _=> exit 1;' \
@@ -50,7 +50,7 @@
fi;\
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;;\
+ \"$(COMP)\" is not poly or sml;;\
esac