From ea2e8d2cf6f0a9bd8a8f359029ac5ac7d96f5d45 Mon Sep 17 00:00:00 2001
From: Peter Dimov <pdimov@gmail.com>
Date: Fri, 22 Feb 2019 19:10:48 +0200
Subject: [PATCH] Remove html/ from .gitignore

---
 doc/.gitignore | 1 -
 1 file changed, 1 deletion(-)

diff --git a/doc/.gitignore b/doc/.gitignore
index 0972e2d..334f513 100644
--- a/doc/.gitignore
+++ b/doc/.gitignore
@@ -1,2 +1 @@
-/html/
 /pdf/