| changeset 17135 | 58f044289dca |
| parent 17098 | dd769bd4d056 |
| child 27063 | d1d35284542f |
--- a/doc-src/Locales/IsaMakefile Fri Aug 19 22:44:36 2005 +0200 +++ b/doc-src/Locales/IsaMakefile Fri Aug 19 22:50:20 2005 +0200 @@ -13,7 +13,7 @@ SRC = $(ISABELLE_HOME)/src OUT = $(ISABELLE_OUTPUT) LOG = $(OUT)/log -USEDIR = $(ISATOOL) usedir -i true -d "" -D generated +USEDIR = $(ISATOOL) usedir -d false -D document ## Locales