1 files changed, 19 insertions, 0 deletions
diff --git a/ci/tools.sh b/ci/tools.sh
index 4eed361b..ecb2e806 100644
--- a/ci/tools.sh
+++ b/ci/tools.sh
@@ -7,6 +7,8 @@
 # http://www.apache.org/licenses/LICENSE-2.0
 ##############################################################################
 
+# include only once
+[ ! -z "$_tools_included" ] && return || readonly _tools_included=true
 
 #######################################
 # Echo printing in yellow bold color
@@ -24,3 +26,20 @@ function echo_info { (
     echo "${@:1:($#-1)}" -e "$yellow_bold${@: -1}$color_off";
   )
 }
+
+#######################################
+# Echo error
+# Arguments:
+#   Same as for echo
+# Returns:
+#   None
+#######################################
+function echo_error { (
+    # don't clutter the script output with the xtrace of the echo command
+    { set +x; } 2> /dev/null
+
+    red_bold='\033[1;31m'
+    color_off='\033[0m'
+    >&2 echo "${@:1:($#-1)}" -e "$red_bold${@: -1}$color_off";
+  )
+}