build(docs): git-ignore generated html documentation

The generated HTML files have been untouched for 7 years. Deleting them definitely for now, in order not to confuse users. Relates to PR #226.
miyuchina · Oct 13, 2024 · 2fbb8b1 · 2fbb8b1
1 parent ac6b3b3
commit 2fbb8b1
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 402 deletions.
diff --git a/docs/.gitignore b/docs/.gitignore
@@ -0,0 +1 @@
+*.html
diff --git a/docs/README.md b/docs/README.md
@@ -1,3 +1,7 @@
-DEPRECATED: This folder used to be the source for project pages. It is not used anymore though.
+Generated documentation
+=======================
 
-This folder's content is updated by running `make docs`.
+This folder is the target for HTML pages generated from the *.md files.
+You can generate it by running `make docs` in the project's root folder.
+
+Note: This folder used to be the source for project pages.
diff --git a/docs/contributing.html b/docs/contributing.html