diff --git a/src/docs/internals/.gitignore b/src/docs/internals/.gitignore new file mode 100644 index 0000000000000000000000000000000000000000..3dc4f08af140eea7f7bd59f6d8c60b646d71277f --- /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