diff --git a/doc/org/index.org b/doc/org/index.org
index 5397a35df..3ab4af84b 100644
--- a/doc/org/index.org
+++ b/doc/org/index.org
@@ -1,29 +1,31 @@
 # -*- coding: utf-8 -*-
 #+TITLE: Spot
 #+SETUPFILE: setup.org
+#+HTML_HEAD_EXTRA: <style>#org-div-home-and-up { display: none; }</style>
 
 Spot is a C++11 library for ω-automata manipulation and model
 checking.  It has the following notable features:
 
-- Support for LTL (several syntaxes supported) and the linear fragment of PSL.
+- Support for LTL (several syntaxes supported) and the linear fragment
+  of PSL.
 - Support for ω-automata with arbitrary acceptance condition.
-- Support for transition-based acceptance (state-based acceptance
-  is supported by a reduction to transition-based acceptance).
+- Support for transition-based acceptance (state-based acceptance is
+  supported by a reduction to transition-based acceptance).
 - The automaton parser can read a stream of automata written in any of
   three syntaxes ([[http://spinroot.com/spin/Man/never.html][never claims]], [[file:hoa.org][HOA]], or [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT]]).
 - Several algorithms for formula manipulation including: simplifying
   formulas, testing implication or equivalence, testing
   stutter-invariance, removing some operators by rewriting, ...
 - Several algorithms for automata manipulation including: product,
-  emptiness checks, simulation-based reductions,
-  minimization of weak-DBA, removal of useless SCCs,
-  acceptance-condition transformations, etc.
-- In addition to the C++ interface, most of its algorithms
-  are usable via [[file:tools.org][command-line tools]], and via Python bindings.
-- One of the command-line tool, called [[file:ltlcross.org][=ltlcross=]] is a rewrite
-  of [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], but with support for PSL and arbitrary acceptance conditions.
-  It could for instance be used to test tools that translate
-  LTL into Rabin automata.
+  emptiness checks, simulation-based reductions, minimization of
+  weak-DBA, removal of useless SCCs, acceptance-condition
+  transformations, etc.
+- In addition to the C++ interface, most of its algorithms are usable
+  via [[file:tools.org][command-line tools]], and via Python bindings.
+- One of the command-line tool, called [[file:ltlcross.org][=ltlcross=]] is a rewrite of
+  [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], but with support for PSL and arbitrary acceptance conditions.
+  It could for instance be used to test tools that translate LTL into
+  Rabin automata.
 
 * Latest version