diff --git a/developer-doc/usingDoxygen.md b/developer-doc/usingDoxygen.md
index d402254fe0e05530c2458c0d32634624a76dbed5..0708548f1102a21fb3bb493e22009d67ea2e8e26 100644
--- a/developer-doc/usingDoxygen.md
+++ b/developer-doc/usingDoxygen.md
@@ -504,9 +504,9 @@ add [makedoc] in the commit log. After ten minutes or so the manual should be up
 and to revert the commit if there are errors! 
 
 It is possible to generate PLUMED manuals for your own personal forks 
-(e.g. USERNAME/plumed) using the procedure above. 
+using a similar procedure as described above. 
 For this to work you need to enable Travis CI for your forked repository 
-and define three environment variables on Travis CI. 
+and define appropriately the environment variables on Travis CI. 
 The github account used to automatically push the generated manuals 
 should be defined using the GIT_BOT variable, 
 preferably this should be a dummy account. A github token
@@ -516,6 +516,6 @@ It is better to make all these environment variable hidden such that they are
 not shown in the public logs on travis-ci.org. 
 To generate a manual for a specific branch you need to create a repository 
 USERNAME/doc-NAMEOFTHEBRANCH and give write access to the account given in 
-the GIT_BOT variable. The generated manuals will be accessible on 
+GIT_BOT. The generated manuals will be accessible on 
 https://USERNAME.github.io/doc-NAMEOFTHEBRANCH. Note that manuals generated in 
-this way will always be unofficial and not shown in search engine results.
+this way will always be labeled as unofficial and not shown in search engine results.