added test for $ISABELLEBIN=source directory, to
avoid isabelle/Pure being mistaken for bin/Pure
--- a/src/CTT/Makefile Wed Jun 01 13:11:40 1994 +0200
+++ b/src/CTT/Makefile Wed Jun 01 13:18:35 1994 +0200
@@ -24,12 +24,18 @@
EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML
$(BIN)/CTT: $(BIN)/Pure $(FILES)
+ if [ -d $${ISABELLEBIN:?}/Pure ];\
+ then echo Bad value for ISABELLEBIN: \
+ $(BIN) is the Isabelle source directory; \
+ exit 1; \
+ fi;\
case "$(COMP)" in \
poly*) echo 'make_database"$(BIN)/CTT"; quit();' \
| $(COMP) $(BIN)/Pure;\
echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/CTT ;;\
sml*) echo 'use"ROOT.ML"; xML"$(BIN)/CTT" banner;' | $(BIN)/Pure ;;\
- *) echo Bad value for ISABELLECOMP;;\
+ *) echo Bad value for ISABELLECOMP: \
+ $(COMP) is not poly or sml;;\
esac
$(BIN)/Pure:
@@ -39,7 +45,8 @@
case "$(COMP)" in \
poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CTT ;;\
sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/CTT;;\
- *) echo Bad value for ISABELLECOMP;;\
+ *) echo Bad value for ISABELLECOMP: \
+ $(COMP) is not poly or sml;;\
esac
.PRECIOUS: $(BIN)/Pure $(BIN)/CTT
--- a/src/FOL/Makefile Wed Jun 01 13:11:40 1994 +0200
+++ b/src/FOL/Makefile Wed Jun 01 13:18:35 1994 +0200
@@ -27,12 +27,18 @@
ex/quant.ML
$(BIN)/FOL: $(BIN)/Pure $(FILES)
+ if [ -d $${ISABELLEBIN:?}/Pure ];\
+ then echo Bad value for ISABELLEBIN: \
+ $(BIN) is the Isabelle source directory; \
+ exit 1; \
+ fi;\
case "$(COMP)" in \
poly*) echo 'make_database"$(BIN)/FOL"; quit();' \
| $(COMP) $(BIN)/Pure;\
echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/FOL;;\
sml*) echo 'use"ROOT.ML"; xML"$(BIN)/FOL" banner;' | $(BIN)/Pure;;\
- *) echo Bad value for ISABELLECOMP;;\
+ *) echo Bad value for ISABELLECOMP: \
+ $(COMP) is not poly or sml;;\
esac
$(BIN)/Pure:
@@ -42,7 +48,8 @@
case "$(COMP)" in \
poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/FOL ;;\
sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/FOL;;\
- *) echo Bad value for ISABELLECOMP;;\
+ *) echo Bad value for ISABELLECOMP: \
+ $(COMP) is not poly or sml;;\
esac
.PRECIOUS: $(BIN)/Pure $(BIN)/FOL