Thanks for the link.
The wiki is missing the article to explain what an "HDMI recorder" is, but anyway, my friend normally only uses his camera to shoot pictures, so it's not worth investing time and money if the camera won't easily record 2h-long videos.