# HG changeset patch
# User wenzelm
# Date 1124356653 -7200
# Node ID dd769bd4d056daea9e5fcac70a943ed48d5e3cf7
# Parent  78f1b66f70a4895feac7ad296a72b72fc9c62a54
usedir: removed option -H;

diff -r 78f1b66f70a4 -r dd769bd4d056 doc-src/LaTeXsugar/IsaMakefile
--- 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
diff -r 78f1b66f70a4 -r dd769bd4d056 doc-src/Locales/IsaMakefile
--- 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