Ignore some TeX output files.

diff --git a/src/docs/internals/.gitignore b/src/docs/internals/.gitignore
new file mode 100644 (file)
index 0000000..3dc4f08
--- /dev/null
+++ b/src/docs/internals/.gitignore
@@ -0,0 +1,10 @@
+/architecture.aux
+/compiler.aux
+/design.aux
+/design.log
+/design.out
+/design.pdf
+/design.toc
+/glossary.aux
+/retargeting.aux
+/run-time.aux