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
diff --git a/Documentation/rest-api-config.txt b/Documentation/rest-api-config.txt
index 5a6c032..6762411 100644
--- a/Documentation/rest-api-config.txt
+++ b/Documentation/rest-api-config.txt
@@ -1163,6 +1163,10 @@
 |`all_users_name`    ||
 Name of the link:config-gerrit.html#gerrit.allUsers[project in which
 meta data of all users is stored].
+|`doc_url`           |optional|
+Custom base URL where Gerrit server documentation is located.
+(Documentation may still be available at /Documentation relative to the
+Gerrit base path even if this value is unset.)
 |`report_bug_url`    |optional|
 link:config-gerrit.html#gerrit.reportBugUrl[URL to report bugs].
 |`report_bug_text`   |optional, not set if default|