diff --git a/doc/org/csv.org b/doc/org/csv.org
index adb85acb9..14a5e56d4 100644
--- a/doc/org/csv.org
+++ b/doc/org/csv.org
@@ -1,7 +1,7 @@
 #+TITLE: Reading and writing CSV files
 #+EMAIL spot@lrde.epita.fr
 #+OPTIONS: H:2 num:nil toc:t
-#+LINK_UP: file:tools.html
+#+LINK_UP: tools.html
 
 This page discusses features available in Spot's command-line
 tools to produce an consume CSV files.
diff --git a/doc/org/dstar2tgba.org b/doc/org/dstar2tgba.org
index 925a019aa..543c2d22b 100644
--- a/doc/org/dstar2tgba.org
+++ b/doc/org/dstar2tgba.org
@@ -1,7 +1,7 @@
 #+TITLE: =dstar2tgba=
 #+EMAIL spot@lrde.epita.fr
 #+OPTIONS: H:2 num:nil toc:t
-#+LINK_UP: file:tools.html
+#+LINK_UP: tools.html
 
 This tool converts deterministic Rabin and Streett automata, presented
 in [[http://www.ltl2dstar.de/docs/ltl2dstar.html][the format output by =ltl2dstar=]], into Büchi automata.
diff --git a/doc/org/genltl.org b/doc/org/genltl.org
index 9e1ff925a..9a6428f7b 100644
--- a/doc/org/genltl.org
+++ b/doc/org/genltl.org
@@ -1,7 +1,7 @@
 #+TITLE: =genltl=
 #+EMAIL spot@lrde.epita.fr
 #+OPTIONS: H:2 num:nil toc:t
-#+LINK_UP: file:tools.html
+#+LINK_UP: tools.html
 
 This tool generates LTL formulas according to scalable patterns.
 These pattern are usually taken from the literature (see the man page
diff --git a/doc/org/init.el.in b/doc/org/init.el.in
index a95af64f9..572bd100a 100644
--- a/doc/org/init.el.in
+++ b/doc/org/init.el.in
@@ -20,6 +20,11 @@
 (setq org-babel-sh-command
       (concat "PATH=@abs_top_builddir@/src/bin" path-separator "$PATH sh"))
 
+(setq org-export-html-home/up-format
+"<div id=\"org-div-home-and-up\" style=\"text-align:center;white-space:nowrap;\">
+ <a accesskey=\"h\" href=\"%s\">UP</a> | <a accesskey=\"H\" href=\"%s\">HOME</a>
+</div>")
+
 (setq org-publish-project-alist
       '(("spot-html"
 	:base-directory "@abs_top_srcdir@/doc/org/"
diff --git a/doc/org/ioltl.org b/doc/org/ioltl.org
index ccca280f5..e4eb7d75c 100644
--- a/doc/org/ioltl.org
+++ b/doc/org/ioltl.org
@@ -1,7 +1,7 @@
 #+TITLE: Common input and output options for LTL/PSL formulas
 #+EMAIL spot@lrde.epita.fr
 #+OPTIONS: H:2 num:nil toc:t
-#+LINK_UP: file:tools.html
+#+LINK_UP: tools.html
 
 Spot supports different syntaxes for LTL/PSL formulas.  This pages
 document the options, common to all tools where it makes sense, that
diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org
index 76f87d99c..84502311f 100644
--- a/doc/org/ltl2tgba.org
+++ b/doc/org/ltl2tgba.org
@@ -1,7 +1,7 @@
 #+TITLE: =ltl2tgba=
 #+EMAIL spot@lrde.epita.fr
 #+OPTIONS: H:2 num:nil toc:t
-#+LINK_UP: file:tools.html
+#+LINK_UP: tools.html
 
 This tool translates LTL or PSL formulas into two kinds of Büchi
 automata, or to monitors.  The default is to output Transition-based
diff --git a/doc/org/ltl2tgta.org b/doc/org/ltl2tgta.org
index 6190232c3..2b6c3e0be 100644
--- a/doc/org/ltl2tgta.org
+++ b/doc/org/ltl2tgta.org
@@ -1,7 +1,7 @@
 #+TITLE: =ltl2tgta=
 #+EMAIL spot@lrde.epita.fr
 #+OPTIONS: H:2 num:nil toc:t
-#+LINK_UP: file:tools.html
+#+LINK_UP: tools.html
 
 This tool generates various form of Testing Automata, i.e., automata
 that observe the /changes/ of atomic propositions, not their values.
diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org
index 0d6e6ec6e..34762984d 100644
--- a/doc/org/ltlcross.org
+++ b/doc/org/ltlcross.org
@@ -1,7 +1,7 @@
 #+TITLE: =ltlcross=
 #+EMAIL spot@lrde.epita.fr
 #+OPTIONS: H:2 num:nil toc:t
-#+LINK_UP: file:tools.html
+#+LINK_UP: tools.html
 
 =ltlcross= is a tool for cross-comparing the output of LTL-to-Büchi
 translators.  It is actually a Spot-based clone of [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], the
diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org
index 7d63a3387..f3cf4ab66 100644
--- a/doc/org/ltlfilt.org
+++ b/doc/org/ltlfilt.org
@@ -1,7 +1,7 @@
 #+TITLE: =ltlfilt=
 #+EMAIL spot@lrde.epita.fr
 #+OPTIONS: H:2 num:nil toc:t
-#+LINK_UP: file:tools.html
+#+LINK_UP: tools.html
 
 This tool is a filter for LTL formulas.  (It will also work with PSL
 formulas.)  It can be used to perform a number of tasks.  Essentially:
diff --git a/doc/org/randltl.org b/doc/org/randltl.org
index 85da5e8db..7faa12176 100644
--- a/doc/org/randltl.org
+++ b/doc/org/randltl.org
@@ -1,7 +1,7 @@
 #+TITLE: =randltl=
 #+EMAIL spot@lrde.epita.fr
 #+OPTIONS: H:2 num:nil toc:t
-#+LINK_UP: file:tools.html
+#+LINK_UP: tools.html
 
 This tool generates random formulas.  By default, it will generate one
 random LTL formula using atomic propositions supplied on the
diff --git a/doc/org/satmin.org b/doc/org/satmin.org
index 5715ceae8..1177b2d2d 100644
--- a/doc/org/satmin.org
+++ b/doc/org/satmin.org
@@ -1,7 +1,7 @@
 #+TITLE: SAT-based Minimization of Deterministic (Generalized) Büchi Automata
 #+EMAIL spot@lrde.epita.fr
 #+OPTIONS: H:2 num:nil toc:t
-#+LINK_UP: file:tools.html
+#+LINK_UP: tools.html
 
 This page explains how to use [[file:ltl2tgba.org][=ltl2tgba=]] or [[file:dstar2tgba.org][=dstar2tgba=]] to minimize
 deterministic automata using a SAT solver.