add favicon in rtd (#3379)

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

diff --git a/docs/conf.py b/docs/conf.py
index e458b554920781b6fafdd35455640bcaa54e28a9..a1b66325a5272129ace5bedd2d5a9ef50402c520 100644 (file)
--- a/docs/conf.py
+++ b/docs/conf.py
@@ -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'

diff --git a/tests/lint/check_file_type.py b/tests/lint/check_file_type.py
index d33cede975085624201eee98c794f9b3e762a74e..ecfad438924a068187e4f5d41a64f62d3150e7f2 100644 (file)
--- a/tests/lint/check_file_type.py
+++ b/tests/lint/check_file_type.py
@@ -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",
    }