diff options
| author | Adam Joseph <adam@westernsemico.com> | 2023-04-13 12:23:02 -0700 |
|---|---|---|
| committer | Adam Joseph <adam@westernsemico.com> | 2023-04-13 12:24:04 -0700 |
| commit | 756e220e1eb71ca1bb7210b82ae694ab62c7a9a2 (patch) | |
| tree | f874e2b7fca2b9b52d260feafe4bb3cb2e457bbd /doc/.gitignore | |
| parent | f53d20ef81e9d98033ccf34509aace3e99dcfbb7 (diff) | |
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.
Diffstat (limited to 'doc/.gitignore')
| -rw-r--r-- | doc/.gitignore | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/.gitignore b/doc/.gitignore index e532ed0eb9c81..b08285995f66f 100644 --- a/doc/.gitignore +++ b/doc/.gitignore @@ -8,3 +8,4 @@ manual-full.xml out result result-* +media |