#5967 output-distance: set device properties in batch driver file

[Han-Wen Nienhuys]

This fixes the output quality of the regtest results.

Previously, the code sets a device by doing

(png16m) finddevice

this put a default device on the stack, ignoring the command-line
arguments. To fix this, specify these settings (HWResolution,
TextAlphaBits, GraphicsAlphaBits) as arguments to the putdeviceprops
call.

https://codereview.appspot.com/560020043

[Anonymous]

Passes make, make check and a full make doc.

[Jonas Hahnfeld]

commit d99780e93bfeafbcafce1c2653eac8e294057e84
Author:     Han-Wen Nienhuys <hanwen@lilypond.org>
AuthorDate: Sat May 9 11:49:03 2020 +0200
Commit:     Han-Wen Nienhuys <hanwen@lilypond.org>
CommitDate: Sun May 10 10:43:12 2020 +0200

    output-distance: set device properties in batch driver file

    This fixes the output quality of the regtest results.

    Previously, the code sets a device by doing

     (png16m) finddevice

    this put a default device on the stack, ignoring the command-line
    arguments.  To fix this, specify these settings (HWResolution,
    TextAlphaBits, GraphicsAlphaBits) as arguments to the putdeviceprops
    call.