From 8076013e80f416939a84d7ffc69255d229205685 Mon Sep 17 00:00:00 2001
From: Michal Sojka <sojka@os.inf.tu-dresden.de>
Date: Wed, 8 Feb 2012 00:54:13 +0100
Subject: [PATCH] Make git ignore generated documentation

---
 src/forb/doc/.gitignore | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 src/forb/doc/.gitignore

diff --git a/src/forb/doc/.gitignore b/src/forb/doc/.gitignore
new file mode 100644
index 00000000..5ccff1a6
--- /dev/null
+++ b/src/forb/doc/.gitignore
@@ -0,0 +1 @@
+html/
-- 
2.39.2