diff --git a/docs/src/DeveloperDocumentation/documentation.md b/docs/src/DeveloperDocumentation/documentation.md
index 833ec6e5a904..80e16a808188 100644
--- a/docs/src/DeveloperDocumentation/documentation.md
+++ b/docs/src/DeveloperDocumentation/documentation.md
@@ -123,7 +123,7 @@ existing entries. An easy way to do that is to add your new BibTeX entry,
 then run [bibtool](http://www.gerd-neugebauer.de/software/TeX/BibTool/en/)
 by invoking it as follows from the root directory of the Oscar.jl repository:
 
-    bibtool docs/oscar_references.bib -o docs/oscar_references.bib
+    bibtool -r .bibtoolsrc docs/oscar_references.bib -o docs/oscar_references.bib
 
 For every pull request on github, the CI checks if running `bibtool` leads to
 changes in the bibliography. If so, this test fails and indicates that the