diff --git a/documentation/dev-manual/dev-manual-common-tasks.xml b/documentation/dev-manual/dev-manual-common-tasks.xml index 13882f2688..43ac532f84 100644 --- a/documentation/dev-manual/dev-manual-common-tasks.xml +++ b/documentation/dev-manual/dev-manual-common-tasks.xml @@ -7218,6 +7218,26 @@ database. + + A live instance of the error reporting server exists at + . + This server exists so that when you want to get help with + build failures, you can submit all of the information on the + failure easily and then point to the URL in your bug report + or send an email to the mailing list. + + If you send error reports to this server, the reports become + publicly visible. + + + + + If you want to set up your own error reporting server, you + can obtain the code from the Git repository at + . + Instructions on how to set it up are in the README document. + + By default, the error reporting tool is disabled. You can enable it by inheriting the