From 9a623367ad77a9a8b5195aef003234b32e00db81 Mon Sep 17 00:00:00 2001 From: Harrison Houghton Date: Tue, 3 Aug 2021 14:45:21 -0400 Subject: [PATCH] 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... --- pkgs/applications/video/manim/default.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pkgs/applications/video/manim/default.nix b/pkgs/applications/video/manim/default.nix index 0f224a5b105..5da81eff50e 100644 --- a/pkgs/applications/video/manim/default.nix +++ b/pkgs/applications/video/manim/default.nix @@ -44,7 +44,7 @@ buildPythonApplication rec { python3 manim.py example_scenes.py $scene -l tail -n 20 files/Tex/*.log # Print potential LaTeX erorrs ${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 '';