# HG changeset patch
# User paulson
# Date 846145817 -7200
# Node ID df91b1610c05d65a0526ae793e5cf18b9a8e735f
# Parent  1d8ae796f3bf885bd1f9bc3e1f1d92a15b9a2e9b
Handles pathnames in ISABELLECOMP

diff -r 1d8ae796f3bf -r df91b1610c05 src/HOL/Auth/Makefile
--- a/src/HOL/Auth/Makefile	Mon Oct 21 11:37:21 1996 +0200
+++ b/src/HOL/Auth/Makefile	Thu Oct 24 10:30:17 1996 +0200
@@ -4,17 +4,17 @@
 #
 BIN = $(ISABELLEBIN)
 COMP = $(ISABELLECOMP)
-NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN Yahalom
+NAMES = Message Shared
 
 FILES = DB-ROOT.ML $(NAMES:%=%.thy) $(NAMES:%=%.ML)
 
 $(BIN)/Auth:   $(BIN)/HOL  $(FILES) 
-	if [ -d $${ISABELLEBIN:?}/Pure ];\
+	@if [ -d $${ISABELLEBIN:?}/Pure ];\
 		then echo Bad value for ISABELLEBIN: \
 			$(BIN) is the Isabelle source directory; \
 			exit 1; \
-		fi;\
-	case "$(COMP)" in \
+	fi
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	echo 'make_database"$(BIN)/Auth"; quit();'  \
 		  | $(COMP) $(BIN)/HOL;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
@@ -35,7 +35,7 @@
 		       | $(BIN)/HOL;\
 		fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml; exit 1;;\
+			\"$(COMP)\" is not poly or sml; exit 1;;\
 	esac
 
 $(BIN)/HOL: