usedir -m brackets;
authorwenzelm
Fri, 15 Dec 2000 18:06:48 +0100
changeset 10682 295a25fee35c
parent 10681 ec76e17f73c5
child 10683 32871d7fbb0a
usedir -m brackets;
doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Fri Dec 15 17:59:45 2000 +0100
+++ b/doc-src/TutorialI/IsaMakefile	Fri Dec 15 18:06:48 2000 +0100
@@ -15,7 +15,7 @@
 SRC = $(ISABELLE_HOME)/src
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
-USEDIR = @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL
+USEDIR = @$(ISATOOL) usedir -m brackets -i true -d dvi -D document $(OUT)/HOL
 
 ## HOL