(v13) ExtraPageDeviceKeys (page device)

This page applies to Harlequin v13.1r0 and later; both Harlequin Core and Harlequin MultiRIP

A dictionary whose contents are merged with any existing ExtraPageDeviceKeys dictionary in the page device, and with the general page device dictionary. This allows for new keys to be added to the page device. The values become the default value of the key which is then subject to change in the usual way by a call to the setpagedevice operator, including the call which adds the new key. If the key already exists, the value in ExtraPageDeviceKeys is ignored.

Default: null .

See also: ExtraMediaSelectionKeys page device key.