--- a/src/HOLCF/Makefile Tue Nov 26 17:49:25 1996 +0100
+++ b/src/HOLCF/Makefile Wed Nov 27 10:31:05 1996 +0100
@@ -34,7 +34,7 @@
#Uses cp rather than make_database because Poly/ML allows only 3 levels
$(BIN)/HOLCF: $(BIN)/HOL $(FILES)
- @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+ @case `basename "$(COMP)"` in \
poly*) cp $(BIN)/HOL $(BIN)/HOLCF; chmod u+w $(BIN)/HOLCF;\
if [ "$${MAKE_HTML}" = "true" ]; \
then echo 'open PolyML; make_html := true; exit_use_dir".";' \
@@ -66,7 +66,7 @@
EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
test: ex/ROOT.ML $(BIN)/HOLCF $(EX_FILES)
- @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+ @case `basename "$(COMP)"` in \
poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
then echo 'make_html := true; exit_use_dir"ex"; quit();' \
| $(COMP) $(BIN)/HOLCF;\
@@ -90,7 +90,7 @@
$(EXPLICIT_DOMAINS_THYS:.thy=.ML)
test2: explicit_domains/ROOT.ML $(BIN)/HOLCF $(EXPLICIT_DOMAINS_FILES)
- @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+ @case `basename "$(COMP)"` in \
poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
then echo 'make_html := true; exit_use_dir"explicit_domains"; quit();' | $(COMP) $(BIN)/HOLCF;\
else echo 'exit_use_dir"explicit_domains"; quit();' \