diff options
Diffstat (limited to 'Build-tools/Bootstrap')
| -rwxr-xr-x | Build-tools/Bootstrap | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/Build-tools/Bootstrap b/Build-tools/Bootstrap index a08006e1eac..7d3ac1322f4 100755 --- a/Build-tools/Bootstrap +++ b/Build-tools/Bootstrap @@ -278,9 +278,8 @@ unless ($opt_skip_manual) &logger($msg); foreach $file qw/internals manual reservedwords/ { - $command= "bk cat $opt_docdir/Docs/$file.texi"; - $command.= " > $target_dir/Docs/$file.texi"; - &run_command($command, "Could not updated $file.texi in $target_dir/Docs/!"); + 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/!"); } } |