From b5efb9b459e7c752226bf327cf0171302c86dbff Mon Sep 17 00:00:00 2001
From: Jean-Francois Dockes <jfd@recoll.org>
Date: Tue, 16 Apr 2013 15:55:31 +0200
Subject: [PATCH] use the xml doc tools

---
 src/makesrcdist.sh | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/makesrcdist.sh b/src/makesrcdist.sh
index fbabdfe4..086a9bad 100644
--- a/src/makesrcdist.sh
+++ b/src/makesrcdist.sh
@@ -103,7 +103,8 @@ fi
 ################################### Documentation
 ###### Html doc
 RECOLLDOC=${RECOLLDOC:=doc/user}
-(cd $RECOLLDOC;make) || exit 1
+(cd $RECOLLDOC; sh xmlmake.sh) || exit 1
+rm -f $RECOLLDOC/usermanual-xml.html $RECOLLDOC/usermanual.xml
 
 ###### Text Doc
 chmod +w README INSTALL