--- a/src/Pure/Makefile Wed Jun 01 08:28:12 1994 +0200
+++ b/src/Pure/Makefile Wed Jun 01 13:11:40 1994 +0200
@@ -38,13 +38,14 @@
cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
echo 'PolyML.use"POLY";use"ROOT";' | $(COMP) $(BIN)/Pure;;\
sml*) if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\
- then echo Bad value for ISABELLEBIN : \
+ then echo Bad value for ISABELLEBIN: \
$(BIN) is not a writable directory; \
exit 1; \
fi;\
echo 'use"NJ.ML"; use"ROOT.ML"; xML"$(BIN)/Pure" banner;'\
| $(COMP);;\
- *) echo Bad value for ISABELLECOMP;;\
+ *) echo Bad value for ISABELLECOMP: \
+ $(COMP) is not poly or sml;;\
esac
.PRECIOUS: $(BIN)/Pure