diff --git a/CHANGES b/CHANGES
index 32104e80215a405362e72d3a3cdeee55fa7fece7..95b6ca7f64810158c5c9dbd9cd2c4d73f867d6ba 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,6 +1,10 @@
 
 * marks an incompatible change
 
+tools
+  * file generated by "why3session html f.mlw" is now
+    "f/why3session.html" and not "f/f.html"
+
 library
   * renamed array.ArraySorted -> array.IntArraySorted
     array.ArraySorted is now generic, with type and order relation parameters
diff --git a/Makefile.in b/Makefile.in
index bb170acfcefd596f85c60345226db82e2db8f15f..d3080f8b41fb32c951c852a2260bc281a986aea3 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -458,10 +458,10 @@ gallery::
 	  why3session html $$x; \
 	  echo "exporting $$f"; \
 	  mkdir -p $(GALLERYDIR)/$$f; \
-	  cp examples/$$f.mlw examples/$$f/$$f.html $(GALLERYDIR)/$$f/; \
+	  cp examples/$$f.mlw examples/$$f/why3session.html $(GALLERYDIR)/$$f/; \
 	  rm -f $(GALLERYDIR)/$$f/$$f.zip; \
 	  cd examples/; \
-	  zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f/$$f.html  $$f; \
+	  zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f; \
 	  cd ..; \
 	done
 
@@ -475,10 +475,10 @@ gallery::
 	mkdir -p $(GALLERYDIR)/$$f; \
 	if test -f examples/$$f.mlw; then cp examples/$$f.mlw $(GALLERYDIR)/$$f/; fi; \
 	if test -f examples/$$f.why; then cp examples/$$f.why $(GALLERYDIR)/$$f/; fi; \
-	cp examples/$$f/$$f.html $(GALLERYDIR)/$$f/; \
+	cp examples/$$f/why3session.html $(GALLERYDIR)/$$f/; \
 	rm -f $(GALLERYDIR)/$$f/$$f.zip; \
 	cd examples/; \
-	zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f/$$f.html  $$f
+	zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f
 
 ########
 # XML DTD validation
diff --git a/doc/manpages.tex b/doc/manpages.tex
index d7a4c45c42bab04e6b5290ae1aff1814eaca8873..bb325bc23cc6cb0841d446e22d03b61e1ef8012a 100644
--- a/doc/manpages.tex
+++ b/doc/manpages.tex
@@ -844,6 +844,10 @@ This command produces a summary of the proof session in HTML syntax.
 There are three styles of output: `table', `simpletree', and
 `jstree'. The default is `table'.
 
+The file generated is named \texttt{why3session.html} and is written
+in the session directory by default (see option \texttt{-o} to
+override this default).
+
 \begin{figure}[t]
 %BEGIN LATEX
 \begin{center}
diff --git a/src/why3session/why3session_html.ml b/src/why3session/why3session_html.ml
index d5f6ffe396fe916736e005b9b0b4560a1f8f2092..a45fd09d1ece2afa916e2bdc8affd714516c1eb5 100644
--- a/src/why3session/why3session_html.ml
+++ b/src/why3session/why3session_html.ml
@@ -78,7 +78,7 @@ let run_file (context : context) print_session fname =
   let basename = Filename.basename project_dir in
   let cout =
     if output_dir = "-" then stdout else
-      open_out (Filename.concat output_dir (basename^".html"))
+      open_out (Filename.concat output_dir ("why3session.html"))
   in
   let fmt = formatter_of_out_channel cout in
   if !opt_context