--- a/src/Cube/Makefile Tue Nov 26 17:49:25 1996 +0100
+++ b/src/Cube/Makefile Wed Nov 27 10:31:05 1996 +0100
@@ -25,7 +25,7 @@
FILES = ROOT.ML Cube.thy Cube.ML
$(BIN)/Cube: $(BIN)/Pure $(FILES)
- @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+ @case `basename "$(COMP)"` in \
poly*) echo 'make_database"$(BIN)/Cube"; quit();' \
| $(COMP) $(BIN)/Pure;\
if [ "$${MAKE_HTML}" = "true" ]; \
@@ -53,7 +53,7 @@
cd ../Pure; $(MAKE)
test: ex.ML $(BIN)/Cube
- @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+ @case `basename "$(COMP)"` in \
poly*) echo 'exit_use"ex.ML"; quit();' | $(COMP) $(BIN)/Cube ;;\
sml*) echo 'exit_use"ex.ML";' | $(BIN)/Cube;;\
*) echo Bad value for ISABELLECOMP: \