From 9c70a3d6a991317543d3553f13126206f85e2ad6 Mon Sep 17 00:00:00 2001
From: Benoit Pierre <benoit.pierre@gmail.com>
Date: Sun, 11 Aug 2024 20:58:27 +0200
Subject: [PATCH] kodev: error out if bash is too old

---
 kodev | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/kodev b/kodev
index 9d3fb2233..bb3311b5a 100755
--- a/kodev
+++ b/kodev
@@ -1,5 +1,10 @@
 #!/usr/bin/env bash
 
+if [[ "${BASH_VERSINFO[0]}" -lt 4 ]]; then
+    echo "incompatible bash version: ${BASH_VERSION}, need >=4.0"
+    exit 1
+fi
+
 ANSI_GREEN="\033[32;1m"
 ANSI_RED="\033[31;1m"