diff -r ec76e17f73c5 -r 295a25fee35c 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