diff --git a/README.linux b/README.linux index f8450f7746f99375ebc85050ff87beab11ff7180..cdb0cfc38bb6bcfaa501cc5d6583906622946c9f 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.