# HG changeset patch
# User lcp
# Date 770469894 -7200
# Node ID f5e5a6b8c4d38aaae6220eb111a49f9edc5a671e
# Parent  d64593bb95d3dff06560ed942b950d4aa4cccd76
added test for $ISABELLEBIN=source directory, to
avoid isabelle/Pure being mistaken for bin/Pure

diff -r d64593bb95d3 -r f5e5a6b8c4d3 Makefile
--- a/Makefile	Wed May 25 13:03:19 1994 +0200
+++ b/Makefile	Wed Jun 01 13:24:54 1994 +0200
@@ -21,8 +21,9 @@
 FILES = ROOT.ML HOL.thy HOL.ML simpdata.ML Ord.thy Ord.ML \
 	fun.ML Set.thy Set.ML subset.ML equalities.ML \
 	Prod.thy Prod.ML Sum.thy Sum.ML WF.thy WF.ML \
-	mono.ML Lfp.thy Lfp.ML Gfp.thy Gfp.ML Nat.thy Nat.ML Sexp.thy \
-	Sexp.ML Univ.thy Univ.ML LList.thy LList.ML List.thy List.ML \
+	mono.ML Lfp.thy Lfp.ML Gfp.thy Gfp.ML Nat.thy Nat.ML \
+        Arith.thy Arith.ML Sexp.thy Sexp.ML Univ.thy Univ.ML \
+        LList.thy LList.ML List.thy List.ML \
 	Datatype.ML \
 	../Provers/classical.ML ../Provers/simplifier.ML \
 	../Provers/splitter.ML ../Provers/ind.ML
@@ -42,12 +43,18 @@
               Subst/UTLemmas.ML Subst/UTLemmas.thy
 
 $(BIN)/HOL:   $(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)/HOL"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
 		echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/HOL ;;\
 	sml*)	echo 'use"ROOT.ML"; xML"$(BIN)/HOL" banner;' | $(BIN)/Pure ;;\
-	*)	echo Bad value for ISABELLECOMP;;\
+	*)	echo Bad value for ISABELLECOMP: \
+                	$(COMP) is not poly or sml;;\
 	esac
 
 $(BIN)/Pure:
@@ -58,7 +65,8 @@
 	poly*)	echo 'use"ex/ROOT.ML"; use"Subst/ROOT.ML"; quit();' \
                         | $(COMP) $(BIN)/HOL ;;\
 	sml*)	echo 'use"ex/ROOT.ML";use"Subst/ROOT.ML";' | $(BIN)/HOL;;\
-	*)	echo Bad value for ISABELLECOMP;;\
+	*)	echo Bad value for ISABELLECOMP: \
+                	$(COMP) is not poly or sml;;\
 	esac
 
 .PRECIOUS:  $(BIN)/Pure  $(BIN)/HOL