HACKING: update instructions to update the manuals at www.gnu.org

Signed-off-by: Stefano Lattarini <stefano.lattarini@gmail.com>

diff --git a/HACKING b/HACKING
index 27eec31..4641d90 100644 (file)
--- a/HACKING
+++ b/HACKING
@@ -258,10 +258,25 @@
   locations.  In case you need to sign with a non-default key, you can
   use "make GNUPLOADFLAGS='--user KEY' git-upload-release".
 
-* For stable releases, update the manuals at www.gnu.org:
-  - Generate manuals, running "make web-manuals".
-  - Copy manuals recursively to web CVS.
-  - Commit in CVS.
+* For stable releases you'll have to update the manuals at www.gnu.org.
+
+  - Generate manuals (with the help of the standard gendocs.sh script):
+
+       make web-manual
+
+    The ready-to-be-uploaded manuals (in several formats) will be left
+    in the 'doc/web-manuals' directory.
+
+  - Commit the updated manuals to web CVS:
+
+      make web-manual-update
+
+    If your local username is different from your username at Savannah,
+    you'll have to override the 'CVS_USER' make variable accordingly;
+    for example:
+
+      make web-manual-update CVS_USER=slattarini
+
   - Check for link errors, fix them, recheck until convergence:
     <http://validator.w3.org/checklink>