diff --git a/documentation/dev-manual/dev-manual-newbie.xml b/documentation/dev-manual/dev-manual-newbie.xml
index 6954b9530d..2da101f80c 100644
--- a/documentation/dev-manual/dev-manual-newbie.xml
+++ b/documentation/dev-manual/dev-manual-newbie.xml
@@ -682,7 +682,7 @@
git branch -D <branch-name>:
Deletes an existing local branch.
You need to be in a local branch other than the one you are deleting
- in order to delete <branch-name>.
+ in order to delete <branch-name>.
git pull: Retrieves information
from an upstream Git
repository and places it in your local Git repository.