--- a/src/Cube/IsaMakefile Thu Mar 20 10:48:00 1997 +0100
+++ b/src/Cube/IsaMakefile Thu Mar 20 10:49:44 1997 +0100
@@ -8,14 +8,13 @@
FILES = ROOT.ML Cube.thy Cube.ML
$(OUT)/Cube: $(OUT)/Pure $(FILES)
- @$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu $(OUT)/Pure Cube
+ @$(ISATOOL) usedir -b $(OUT)/Pure Cube
@chmod -w $@
$(OUT)/Pure:
@cd ../Pure; $(ISATOOL) make
-test: ex.ML $(OUT)/Cube
- @$(ISABELLE) -e 'make_html := $(ISABELLE_HTML); use"ex.ML"; quit();' \
- -rq $(OUT)/Cube
+test: ex/ROOT.ML ex/ex.ML $(OUT)/Cube
+ @$(ISATOOL) usedir $(OUT)/Cube ex
.PRECIOUS: $(OUT)/Pure $(OUT)/Cube