doc: simplify doc redirection messages

We have directives in conf.py to create redirect links for docs that
have been moved around because of content reorganization.  Reduce the
number of messages written out while debugging was going on and add some
comments to conf.py to explain how the directive works.

Signed-off-by: David B. Kinder <david.b.kinder@intel.com>

doc/conf.py

@@ -292,10 +292,13 @@
 htmlhelp_basename = 'zephyrdoc'
 
 
-# Custom added feature to allow redirecting old URLs
+# Custom added feature to allow redirecting old URLs (caused by
+# reorganizing doc directories)
 #
 # list of tuples (old_url, new_url) for pages to redirect
-# (URLs should be relative to document root, only)
+#
+# URLs must be relative to document root (with NO leading slash),
+# and without the html extension)
 html_redirect_pages = [
         ('contribute/contribute_guidelines', 'contribute/index'),
         ('application/application', 'application/index.rst'),

doc/extensions/zephyr/html_redirects.py

@@ -56,14 +56,12 @@ def create_redirect_pages(app, docname):
         return  # only relevant for standalone HTML output
 
     for (old_url, new_url) in app.config.html_redirect_pages:
-        print("Creating redirect %s to %s..." % (old_url, new_url))
         if old_url.startswith('/'):
-            print("Stripping leading / from URL in config file...")
             old_url = old_url[1:]
+        print("Creating redirect: %s.html to %s.html" % (old_url, new_url))
 
         new_url = app.builder.get_relative_uri(old_url, new_url)
         out_file = app.builder.get_outfilename(old_url)
-        print("HTML file %s redirects to relative URL %s" % (out_file, new_url))
 
         out_dir = os.path.dirname(out_file)
         if not os.path.exists(out_dir):