Rename html/ directory to docs/ for GitHub Pages compatibility.

[pgbigm/pg_bigm.git] / docs / pg_bigm_en-1-1.html

diff --git a/html/pg_bigm_en-1-1.html b/docs/pg_bigm_en-1-1.html
similarity index 100%
rename from html/pg_bigm_en-1-1.html
rename to docs/pg_bigm_en-1-1.html