# HG changeset patch
# User diego
# Date 1260752253 0
# Node ID f5dc9e81586547bfd6c94fdf311fe0245c54caf1
# Parent  113ab3d1feab130b67f50dffe0723ea95ae9ac60
Use variable for HTML stylesheet so individual languages can use their own.

diff -r 113ab3d1feab -r f5dc9e815865 DOCS/xml/Makefile.inc
--- a/DOCS/xml/Makefile.inc	Mon Dec 14 00:42:46 2009 +0000
+++ b/DOCS/xml/Makefile.inc	Mon Dec 14 00:57:33 2009 +0000
@@ -36,7 +36,7 @@
 	../xmllint.sh $<
 
 $(HTMLDIR)/default.css:
-	cp -f ../default.css $(@D)
+	cp -f $(HTML_STYLESHEET) $(@D)
 
 $(HTMLDIR)/index.html: main.xml $(CHUNK_XSL_DEPS) $(SYMLINKS_DEPS) xmllint $(HTMLDIR)/default.css
 	../xsltproc.sh $(HTMLDIR)/ $(HTML_CHUNK_XSL) $<