# HG changeset patch
# User wenzelm
# Date 858851384 -3600
# Node ID ebeacfa0e56b7097ab6137e166677d8e7b5cb817
# Parent  b47926f28b214e8e4aaa75e4e46522811fca9ca2
isatool usedir;

diff -r b47926f28b21 -r ebeacfa0e56b src/Cube/IsaMakefile
--- 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