doc: Add man page of para_play to documentation web page.

In December 2012 para_play was merged to master but we missed to
update the web page accordingly.

diff --git a/web/documentation.in.html b/web/documentation.in.html
index 4d63a08fb9721ff0d0f824eda66ac5e4fb0b49e5..f292af25d723764f18e555e8daac714089f3d7f5 100644 (file)
--- a/web/documentation.in.html
+++ b/web/documentation.in.html
@@ -30,6 +30,7 @@
        [<a href="para_write.man.html">para_write</a>]
        [<a href="para_gui.man.html">para_gui</a>]
        [<a href="para_fade.man.html">para_fade</a>]
        [<a href="para_write.man.html">para_write</a>]
        [<a href="para_gui.man.html">para_gui</a>]
        [<a href="para_fade.man.html">para_fade</a>]

+       [<a href="para_play.man.html">para_play</a>]

 </p>
 
 <h2> Source code documentation </h2>
 </p>
 
 <h2> Source code documentation </h2>