Uploading media

We use the uploading trick detailed here. Also, we often convert videos into gifs using the shell script video_to_gif.sh.

---

Last update: July 23, 2023
Created: July 23, 2023