diff --git a/docs/scripts/generate_web.php b/docs/scripts/generate_web.php
index 0b501076..fa4ac4d9 100755
--- a/docs/scripts/generate_web.php
+++ b/docs/scripts/generate_web.php
@@ -17,6 +17,8 @@
   +----------------------------------------------------------------------+
   | Small hack to generate the manual for the web                        |
   +----------------------------------------------------------------------+
+
+  $Id$
 */
 
 set_time_limit(0);