Fix colours in RTD [ci skip]

felix-lang · Nov 25, 2017 · 6835d23 · 6835d23
1 parent 5188f7f
commit 6835d23
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 2 deletions.
diff --git a/doc/tutorial/_templates/layout.html b/doc/tutorial/_templates/layout.html
@@ -7,5 +7,10 @@
       }
       });
     </script>
+<style> 
+span.k {color:green;} 
+span.s {color:black;} 
+</style> 
+
 {% endblock %}
 
diff --git a/doc/tutorial/conf.py b/doc/tutorial/conf.py
@@ -102,7 +102,7 @@
 
 # The theme to use for HTML and HTML Help pages.  See the documentation for
 # a list of builtin themes.
-html_theme = 'classic'
+html_theme = 'sphinx_rtd_theme'
 
 # Theme options are theme-specific and customize the look and feel of a theme
 # further.  For a list of options available for each theme, see the

diff --git a/doc/tutorial/gui05.rst b/doc/tutorial/gui05.rst
@@ -5,6 +5,8 @@ A *window manager* is a component that automates
 distribution of message such as mouse clicks and key
 presses to one of several event handlers.
 
+.. image:: gui05.jpeg
+
 The initial windows
 -------------------
 
@@ -84,7 +86,6 @@ The same as before!
 The Window manager
 ------------------
 
-.. image:: gui05.jpeg
 
 Noe for the fun bit. First, our mainline creates a window manager
 object: