From: Bruno Haible <bruno@clisp.org>
Date: Wed, 3 Oct 2007 12:07:57 +0000 (+0200)
Subject: Add gnulib.html, generated by "make html".
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=868a38673080c61a27194ad57e833e4460a21729;p=pspp

Add gnulib.html, generated by "make html".
---

diff --git a/doc/.gitignore b/doc/.gitignore
index 0f62408523..175321e78f 100644
--- a/doc/.gitignore
+++ b/doc/.gitignore
@@ -13,3 +13,4 @@ gnulib.info
 gnulib.info-1
 gnulib.info-2
 gnulib.info-3
+gnulib.html