diff --git a/README.linux b/README.linux index 193976cf0b8341a1dc748fb5e3261a643596f921..363fadf0016150a1504002bcc54d3bdef8b4945b 100644 --- a/README.linux +++ b/README.linux @@ -32,7 +32,7 @@ LICENSING := no USAGE_STATS := no -Several build options are possible; for details on options , please read through the Makefile.cfg. +Several build options are possible; for details on options please read through the Makefile.cfg. Options can be overridden by the content of a file named Makefile.personal which can be used to adapt to local installation directories, change config options etc. Below, a small number of typical scenarios are presented.