The right extension is now always used, and if the codecs are
there, ffmpeg will render the animation.

For the future, we should probably implement a way to set the
framerate for animation...