Replying to myself, in case this can be of use to anyone.
I got this problem solved by using the following ffmpeg incantation:
ffmpeg -i 1.mkv -i 2.m2ts -filter_complex "\
[0:v]scale=1920:1080:force_original_aspect_ratio=decrease,setsar=1,\
pad=1920:1080:(ow-iw)/2:(oh-ih)/2[0v]; \
After some googling I was able to find out how to use ffmpeg to convert MKV
videos in H.264 format to MKV videos in H.265 format. I looked into this
because I have a lot of H.264 videos, which I would like to reduce in size,
as H.265 can reportedly do.
However, in my search I also found out
