diff options
| author | unknown <joerg@mysql.com> | 2005-03-30 17:59:36 +0200 |
|---|---|---|
| committer | unknown <joerg@mysql.com> | 2005-03-30 17:59:36 +0200 |
| commit | 0630d62f2dd97dcea4fb4cc1b4742c6de93c80cd (patch) | |
| tree | 344021e11d618eb5f9c024c694be02fcccba4c9f /Build-tools | |
| parent | 5ac4670bf7f17374e8bae1bd27625ccabc1eac82 (diff) | |
| download | mariadb-git-0630d62f2dd97dcea4fb4cc1b4742c6de93c80cd.tar.gz | |
Ensure 'texi2html' is taken from the Docs tree, not to miss any corrections.
Diffstat (limited to 'Build-tools')
| -rwxr-xr-x | Build-tools/Bootstrap | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/Build-tools/Bootstrap b/Build-tools/Bootstrap index 64f865362ca..f9bb2170156 100755 --- a/Build-tools/Bootstrap +++ b/Build-tools/Bootstrap @@ -273,7 +273,7 @@ if (defined $opt_changelog) } # -# Add the latest manual from the mysqldoc tree +# Add the latest manual and tool from the mysqldoc tree # unless ($opt_skip_manual) { @@ -283,6 +283,8 @@ unless ($opt_skip_manual) system ("bk cat $opt_docdir/Docs/$file.texi > $target_dir/Docs/$file.texi") == 0 or &abort("Could not update $file.texi in $target_dir/Docs/!"); } + &run_command("cp $opt_docdir/Docs/Support/texi2html $target_dir/Docs/Support", + "Could not copy $opt_docdir/Docs/Support/texi2html!"); &run_command("rm -f $target_dir/Docs/Images/Makefile*", "Could not remove Makefiles in $target_dir/Docs/Images/!"); |