diff options
| author | lenz@kallisto.local <> | 2003-11-18 16:48:02 +0100 |
|---|---|---|
| committer | lenz@kallisto.local <> | 2003-11-18 16:48:02 +0100 |
| commit | 578a677468faf8ebca289d95167d93ef272b239f (patch) | |
| tree | 0bdc2d73ca562d2af885cbed8a437f026e821e1d /Build-tools | |
| parent | 6d350964dc9f3fe105521c9e4f791443c25e121a (diff) | |
| download | mariadb-git-578a677468faf8ebca289d95167d93ef272b239f.tar.gz | |
- internals.texi will now be part of the source distribution. However,
as this is a document that belongs to the mysqldoc tree, it needs to
be copied over manually (using the Bootstrap script), before doing an
official release distribution. The file Docs/internals.texi in this tree
is only a dummy file to keep "make dist" happy.
Diffstat (limited to 'Build-tools')
| -rwxr-xr-x | Build-tools/Bootstrap | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Build-tools/Bootstrap b/Build-tools/Bootstrap index 94446d9880f..17b15d190b0 100755 --- a/Build-tools/Bootstrap +++ b/Build-tools/Bootstrap @@ -276,7 +276,7 @@ unless ($opt_skip_manual) { $msg= "Adding manual.texi"; &logger($msg); - $command= "install -m 644 $opt_docdir/Docs/{manual,reservedwords}.texi"; + $command= "install -m 644 $opt_docdir/Docs/{internals,manual,reservedwords}.texi"; $command.= " $target_dir/Docs/"; &run_command($command, "Could not update the manual in $target_dir/Docs/!"); } |