From c1b9db6b3efecc92a02082c836fbfe1168151e38 Mon Sep 17 00:00:00 2001
From: Dirk Zimoch <dirk.zimoch@psi.ch>
Date: Thu, 16 Feb 2023 12:03:02 +0100
Subject: [PATCH] make sure extglob is enabled for shell

---
 App/tools/driver.makefile | 1 +
 1 file changed, 1 insertion(+)

diff --git a/App/tools/driver.makefile b/App/tools/driver.makefile
index c347235..76e601f 100644
--- a/App/tools/driver.makefile
+++ b/App/tools/driver.makefile
@@ -341,6 +341,7 @@ ${CONFIG}/CONFIG:
 EB:=${EPICS_BASE}
 TOP:=${EPICS_BASE}
 -include ${CONFIG}/CONFIG
+SHELL = /bin/bash -O extglob
 BASE_CPPFLAGS=
 EPICS_BASE:=${EB}
 COMMON_DIR = O.${EPICSVERSION}_Common