diff --git a/tools/generate-docs b/tools/generate-docs
index bdccc7fd1b35..e52ec5605c4c 100755
--- a/tools/generate-docs
+++ b/tools/generate-docs
@@ -1,19 +1,6 @@
 #!/bin/bash -e
 
-# PRELUDE: FIND THE REAL PATH OF THIS FILE
-pushd . > '/dev/null';
-SCRIPT_PATH="${BASH_SOURCE[0]:-$0}";
-
-while [ -h "$SCRIPT_PATH" ];
-do
-    cd "$( dirname -- "$SCRIPT_PATH"; )";
-    SCRIPT_PATH="$( readlink -f -- "$SCRIPT_PATH"; )";
-done
-
-cd "$( dirname -- "$SCRIPT_PATH"; )" > '/dev/null';
-SCRIPT_PATH="$( pwd; )";
-popd  > '/dev/null';
-# END PRELUDE
+# This script must be executed on the project's root.
 
 # Navigate to the docs directory
 cd ./docs/