Use bootstrap script to set up doc tree.

diff --git a/dist/make-src-files b/dist/make-src-files
index e98b05fade1ebab062b67719cadf8809abd06e2b..5f30edd95324854584d8eb2544c7fe271a91f2e8 100755 (executable)
--- a/dist/make-src-files
+++ b/dist/make-src-files
@@ -69,7 +69,7 @@ cleanup_file "${DIST_DIR}"
 
 notify "Configuring the source tree"
 run_command "${SRC_OUT}"-config "${DIST_DIR}"/src ./Setup.sh
-run_command_append "${SRC_OUT}"-config "${DIST_DIR}"/doc autoconf
+run_command_append "${SRC_OUT}"-config "${DIST_DIR}"/doc ./bootstrap
 
 notify "Creating archive file"
 make_tar_file "${SRC_OUT}" "${DIST_DIR}"