--- a/doc-src/LaTeXsugar/IsaMakefile Thu Aug 18 11:17:32 2005 +0200
+++ b/doc-src/LaTeXsugar/IsaMakefile Thu Aug 18 11:17:33 2005 +0200
@@ -14,7 +14,7 @@
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
-USEDIR = $(ISATOOL) usedir -v true -i false -g false -d false -D document -H false
+USEDIR = $(ISATOOL) usedir -v true -i false -g false -d false -D document
## Sugar
--- a/doc-src/Locales/IsaMakefile Thu Aug 18 11:17:32 2005 +0200
+++ b/doc-src/Locales/IsaMakefile Thu Aug 18 11:17:33 2005 +0200
@@ -13,7 +13,7 @@
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
-USEDIR = $(ISATOOL) usedir -i true -d "" -H false -D generated
+USEDIR = $(ISATOOL) usedir -i true -d "" -D generated
## Locales
@@ -23,7 +23,8 @@
HOL:
@cd $(SRC)/HOL; $(ISATOOL) make HOL
-$(LOG)/HOL-Locales.gz: $(OUT)/HOL Locales/ROOT.ML Locales/Locales.thy Locales/document/root.tex Locales/document/root.bib
+$(LOG)/HOL-Locales.gz: $(OUT)/HOL Locales/ROOT.ML Locales/Locales.thy \
+ Locales/document/root.tex Locales/document/root.bib
@$(USEDIR) $(OUT)/HOL Locales