Existing manim package has been incorrectly named manim, although on PyPi it is
called manimlib. It is now developed under the name manimgl, so the PyPi
package manimlib will receive no further updates. The new manim
package in nixpkgs is now the Manim Community Edition.
Turns out that O and 0 are different characters, even though they look
the same in many monospace fonts (including mine). Unfortunately, they
look very different to grep -F...
After making `ffmpeg` point to the latest `ffmpeg_4`, all packages that
used `ffmpeg` without requiring a specific version now use ffmpeg_3
explicitly so they shouldn't change.
