Installing in $HOME should not be the default advice

We ourselves install most of the time in /opt, and asking people to open
their homefolder can yield other problems.

Left the mention of prefix so people are aware they can pick another
location to keep the documentation clear.

(cherry picked from commit df281ac)

Author: vmcj

doc/manual/install-domserver.rst

@@ -57,9 +57,9 @@ taken than simply running ``./configure && make && make install``.
 
 After installing the required software as described above, run configure.
 In this example to install DOMjudge in the directory ``domjudge`` under
-your home directory::
+`/opt`::
 
-  ./configure --prefix=$HOME/domjudge
+  ./configure --prefix=/opt/domjudge
   make domserver
   sudo make install-domserver
 

doc/manual/install-judgehost.rst

@@ -54,10 +54,9 @@ These instructions assume a release `tarball <https://www.domjudge.org/download>
 for instructions to build from git sources.
 
 After installing the software listed above, run configure. In this
-example to install DOMjudge in the directory ``domjudge`` under your
-home directory::
+example to install DOMjudge in the directory ``domjudge`` under `/opt`::
 
-  ./configure --prefix=$HOME/domjudge
+  ./configure --prefix=/opt/domjudge
   make judgehost
   sudo make install-judgehost