Commit 756e220e authored by Adam Joseph's avatar Adam Joseph
Browse files

doc/.gitignore: add media

These files are generated when you run `nix-shell --command make`
and are likely to be committed by accident.  Let's help people avoid
that.
parent f53d20ef
Loading
Loading
Loading
Loading
+1 −0
Original line number Diff line number Diff line
@@ -8,3 +8,4 @@ manual-full.xml
out
result
result-*
media