From 51a09de81d10714d0d1a03e4eab028e994cb82e1 Mon Sep 17 00:00:00 2001
From: Pavel Campr <pavel@campr.cz>
Date: Fri, 14 Nov 2014 08:31:34 +0100
Subject: [PATCH] fixed filename in build_docs.sh

---
 scripts/build_docs.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/build_docs.sh b/scripts/build_docs.sh
index f8ace0ead43..0e28bd71631 100755
--- a/scripts/build_docs.sh
+++ b/scripts/build_docs.sh
@@ -3,7 +3,7 @@
 
 PORT=${1:-4000}
 
-echo "usage: build.sh [port]"
+echo "usage: build_docs.sh [port]"
 
 # Find the docs dir, no matter where the script is called
 ROOT_DIR="$( cd "$(dirname "$0")"/.. ; pwd -P )"