From: Ben Pfaff <blp@cs.stanford.edu>
Date: Wed, 2 Sep 2020 06:02:44 +0000 (-0700)
Subject: doc/manual: Remove gitignore file in otherwise empty directory.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=be0d215fc59eee406e357e833fa0155e2d81abdf;p=pspp

doc/manual: Remove gitignore file in otherwise empty directory.

I added this by mistake some time ago.  It's not useful.
---

diff --git a/doc/manual/.gitignore b/doc/manual/.gitignore
deleted file mode 100644
index 524b61ed3b..0000000000
--- a/doc/manual/.gitignore
+++ /dev/null
@@ -1,5 +0,0 @@
-pspp.dvi.gz
-pspp.info.tar.gz
-pspp.pdf
-pspp.txt
-pspp.txt.gz