# HG changeset patch
# User diego
# Date 1260740611 0
# Node ID c5ddf34d6f5721a0ddb416a5b5d358b668b4f645
# Parent  caaabaff1fe4fe4f8e40a0f6af8e4381caa70fc4
xmllint.sh is not a phony target.

diff -r caaabaff1fe4 -r c5ddf34d6f57 DOCS/xml/Makefile
--- a/DOCS/xml/Makefile	Sun Dec 13 21:33:24 2009 +0000
+++ b/DOCS/xml/Makefile	Sun Dec 13 21:43:31 2009 +0000
@@ -62,4 +62,4 @@
 
 distclean: clean releaseclean
 
-.PHONY: all help html-chunked* html-single* xmllint* *clean*
+.PHONY: all help html-chunked* html-single* xmllint xmllint-* *clean*