manim: fix

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...
This commit is contained in:
Harrison Houghton 2021-08-03 14:45:21 -04:00 committed by Robert Helgesson
parent a79a5b880c
commit 9a623367ad

View File

@ -44,7 +44,7 @@ buildPythonApplication rec {
python3 manim.py example_scenes.py $scene -l python3 manim.py example_scenes.py $scene -l
tail -n 20 files/Tex/*.log # Print potential LaTeX erorrs tail -n 20 files/Tex/*.log # Print potential LaTeX erorrs
${file}/bin/file videos/example_scenes/480p15/$scene.mp4 \ ${file}/bin/file videos/example_scenes/480p15/$scene.mp4 \
| tee | grep -F "ISO Media, MP4 Base Media v1 [IS0 14496-12:2003]" | tee | grep -F "ISO Media, MP4 Base Media v1 [ISO 14496-12:2003]"
done done
''; '';