- Output redirection does not work with run_command(), use system()

   instead.

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/!");
 	}
 }