aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorBen Gamari <ben@smart-cactus.org>2016-05-16 14:55:17 +0200
committerBen Gamari <ben@smart-cactus.org>2016-05-16 14:55:17 +0200
commit1bfcca3f2212e1f8e527ad3a2c4bb48aef082ff9 (patch)
tree9932eec88f07f9563a88417cacfb822e4e512747
parentc277db2271e22e3b8fa1afeaf42ffc6988a48720 (diff)
parentcec21957001143794e71bcd9420283df18e7de40 (diff)
Merge remote-tracking branch 'origin/master' into ghc-head
-rw-r--r--.gitmodules3
m---------doc/alabaster0
-rw-r--r--doc/conf.py1
3 files changed, 4 insertions, 0 deletions
diff --git a/.gitmodules b/.gitmodules
new file mode 100644
index 00000000..ac3559da
--- /dev/null
+++ b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "doc/alabaster"]
+ path = doc/alabaster
+ url = git://github.com/bitprophet/alabaster.git
diff --git a/doc/alabaster b/doc/alabaster
new file mode 160000
+Subproject aabda1182083d21b6d9bafb53ea8a99eb4be4cf
diff --git a/doc/conf.py b/doc/conf.py
index d6b8bda8..6e73eb5c 100644
--- a/doc/conf.py
+++ b/doc/conf.py
@@ -29,6 +29,7 @@ pygments_style = 'tango'
# -- Options for HTML output ----------------------------------------------
+html_theme_path = ['./alabaster']
html_theme = 'alabaster'
htmlhelp_basename = 'Haddockdoc'