From 756e220e1eb71ca1bb7210b82ae694ab62c7a9a2 Mon Sep 17 00:00:00 2001 From: Adam Joseph Date: Thu, 13 Apr 2023 12:23:02 -0700 Subject: [PATCH] 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. --- doc/.gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/doc/.gitignore b/doc/.gitignore index e532ed0eb9c8..b08285995f66 100644 --- a/doc/.gitignore +++ b/doc/.gitignore @@ -8,3 +8,4 @@ manual-full.xml out result result-* +media