Add optional video conversion to mp4 or lossless mkv.

[zephyr]

Size and quality of game.mp4 is roughly the same as game.webm, but the format may currently be supported by more output devices.

Size of game_raw.mkv is roughly one-fifth of game_raw.mov, yet still twice as big as game.webm, and more expensive to compute.