doc-src/Locales/Makefile
changeset 17135 58f044289dca
parent 16168 adb83939177f
child 26916 3331d559feaf
--- a/doc-src/Locales/Makefile	Fri Aug 19 22:44:36 2005 +0200
+++ b/doc-src/Locales/Makefile	Fri Aug 19 22:50:20 2005 +0200
@@ -8,7 +8,7 @@
 
 ## paths
 
-TEXPATH = Locales/generated/:
+TEXPATH = Locales/document/:
 
 ## dependencies
 
@@ -16,10 +16,10 @@
 
 NAME = locales
 
-FILES = Locales/generated/root.tex Locales/generated/root.bib \
-  Locales/generated/session.tex Locales/generated/Locales.tex \
-  Locales/generated/isabelle.sty Locales/generated/isabellesym.sty \
-  Locales/generated/pdfsetup.sty 
+FILES = Locales/document/root.tex Locales/document/root.bib \
+  Locales/document/session.tex Locales/document/Locales.tex \
+  Locales/document/isabelle.sty Locales/document/isabellesym.sty \
+  Locales/document/pdfsetup.sty 
 
 dvi: $(NAME).dvi