Make documentation base URL configurable

Administrators may want to store documentation on a separate static
content server from the actual Gerrit server, or use a reverse proxy
configuration to serve the docs from somewhere other than
/Documentation. Allow this with a new configuration option,
gerrit.docUrl.

For parallelism while loading the app we still probe
/Documentation/index.html; the result of this request is simply
discarded if the server config endpoint later returns a configured
documentation URL.

Change-Id: I98477e3539f5c6271014cedd03354c3345e7379b
diff --git a/Documentation/config-gerrit.txt b/Documentation/config-gerrit.txt
index 723e24c..f95d9d1 100644
--- a/Documentation/config-gerrit.txt
+++ b/Documentation/config-gerrit.txt
@@ -1695,6 +1695,18 @@
 by the system administrator, and might not even be running on the
 same host as Gerrit.
 
+[[gerrit.docUrl]]gerrit.docUrl::
++
+Optional base URL for documentation, under which one can find
+"index.html", "rest-api.html", etc. Used as the base for the fixed set
+of links in the "Documentation" tab. A slash is implicitly appended.
+(For finer control over the top menu, consider writing a
+link:dev-plugins.html#top-menu-extensions[plugin].)
++
+If unset or empty, the documentation tab will only be shown if
+`/Documentation/index.html` can be reached by the browser at app load
+time.
+
 [[gerrit.installCommitMsgHookCommand]]gerrit.installCommitMsgHookCommand::
 +
 Optional command to install the `commit-msg` hook. Typically of the