# HG changeset patch
# User wenzelm
# Date 1001679001 -7200
# Node ID 9ab0792b2da43186836c66fe1e384014aa5e35ca
# Parent  ee1247ba494124f29078bd4ccfaaef13efe73fe3
tuned;

diff -r ee1247ba4941 -r 9ab0792b2da4 doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Fri Sep 28 14:04:14 2001 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Fri Sep 28 14:10:01 2001 +0200
@@ -15,8 +15,10 @@
 SRC = $(ISABELLE_HOME)/src
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
-USEDIR = @$(ISATOOL) usedir -m brackets -i true -d dvi -D document $(OUT)/HOL
-REALUSEDIR = @$(ISATOOL) usedir -m brackets -i true -d dvi -D document $(OUT)/HOL-Real
+OPTIONS = -m brackets -i true -d dvi -D document
+USEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL
+REALUSEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL-Real
+
 
 ## HOL