projects / pintos-anon / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 9a4067d)
Ignore files produced by "makeinfo".
authorBen Pfaff <blp@cs.stanford.edu>
Sun, 9 Nov 2008 23:42:02 +0000 (15:42 -0800)
committerBen Pfaff <blp@cs.stanford.edu>
Sun, 9 Nov 2008 23:42:02 +0000 (15:42 -0800)
doc/.gitignore patch | blob | history

diff --git a/doc/.gitignore b/doc/.gitignore
index fbb33467cf0dfe54cb55aea71865b2fb60f10bf5..0f581122249b53b7e9e12385f53c4d7c6e95925d 100644 (file)
--- a/doc/.gitignore
+++ b/doc/.gitignore
@@ -9,6 +9,9 @@
 *.toc
 *.tp
 *.vr
+/pintos.fns
+/pintos.tps
+/pintos.vrs
 mlfqs1.pdf
 mlfqs1.png
 mlfqs2.pdf
Pintos public repository