add favicon in rtd (#3379)
authorSheng Zha <szha@users.noreply.github.com>
Mon, 17 Jun 2019 16:52:31 +0000 (09:52 -0700)
committerTianqi Chen <tqchen@users.noreply.github.com>
Mon, 17 Jun 2019 16:52:31 +0000 (09:52 -0700)
docs/_static/img/tvm-logo-square.png [new file with mode: 0644]
docs/conf.py
tests/lint/check_file_type.py

diff --git a/docs/_static/img/tvm-logo-square.png b/docs/_static/img/tvm-logo-square.png
new file mode 100644 (file)
index 0000000..37822d1
Binary files /dev/null and b/docs/_static/img/tvm-logo-square.png differ
index e458b55..a1b6632 100644 (file)
@@ -165,6 +165,8 @@ html_theme_options = {
 
 html_logo = "_static/img/tvm-logo-small.png"
 
+html_favicon = "_static/img/tvm-logo-square.png"
+
 
 # Output file base name for HTML help builder.
 htmlhelp_basename = project + 'doc'
index d33cede..ecfad43 100644 (file)
@@ -107,6 +107,7 @@ ALLOW_SPECIFIC_FILE = {
     # documentation related files
     "docs/_static/css/tvm_theme.css",
     "docs/_static/img/tvm-logo-small.png",
+    "docs/_static/img/tvm-logo-square.png",
    }