1 files changed, 18 insertions, 1 deletions
diff --git a/ci/tools.sh b/ci/tools.sh
index ecb2e806..45db67e1 100644
--- a/ci/tools.sh
+++ b/ci/tools.sh
@@ -28,7 +28,7 @@ function echo_info { (
 }
 
 #######################################
-# Echo error
+# Echo error (to stderr)
 # Arguments:
 #   Same as for echo
 # Returns:
@@ -43,3 +43,20 @@ function echo_error { (
     >&2 echo "${@:1:($#-1)}" -e "$red_bold${@: -1}$color_off";
   )
 }
+
+#######################################
+# Echo warning (to stderr)
+# Arguments:
+#   Same as for echo
+# Returns:
+#   None
+#######################################
+function echo_warning { (
+    # don't clutter the script output with the xtrace of the echo command
+    { set +x; } 2> /dev/null
+
+    red_italic='\033[3;91m'
+    color_off='\033[0m'
+    >&2 echo "${@:1:($#-1)}" -e "$red_italic${@: -1}$color_off";
+  )
+}