# HG changeset patch
# User wenzelm
# Date 976900008 -3600
# Node ID 295a25fee35c66d42b51a3d871ff61b25c01dcd1
# Parent  ec76e17f73c5320e3c1224a3cb444e9c4b9c95cf
usedir -m brackets;

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