PrintTo( filename, obj1,
obj2... )
PrintTo works like Print, except that the output is
printed to the file with the name filename instead of the standard
output. This file must of course be writable by GAP,
otherwise an error is signalled. Note that PrintTo will
overwrite the previous contents of this file if it already existed. AppendTo
can be used to append to a file (see AppendTo).
The special file name "*stdout*" can be used to print to the
standard output. This is equivalent to a plain Print, except
that a plain Print that is executed while evaluating an argument
to a PrintTo call will also print to the output file opened by
the last PrintTo call, while PrintTo( "*stdout*", obj1,
obj2... ) always prints to the standard output. The special
file name "*errout*" can be used to print to the standard error
output file, which is usually connected with the terminal, even if the
standard output was redirected.
There is an operating system dependent maximum to the number of output files that may be open at once, usually this is 14.