This is a useful command for turning mp4 videos into animated gifs.
$ ffmpeg -i source.mp4 -r 15 -vf scale=1000:-1 destination.gif
You can then edit them in GIMP if needed. Be sure to check the “animate” box when exporting from GIMP (ctrl-shift-e
).