From 7233b3b1f88cdc8bc9b4e2c0235ab158ecbe9913 Mon Sep 17 00:00:00 2001
From: PHO <pho@cielonegro.org>
Date: Thu, 2 Nov 2023 23:37:12 +0900
Subject: [PATCH] Use '[' instead of '[[' because the latter is a Bash-ism

It doesn't work on platforms where /bin/sh is something other than Bash.
---
 rts/configure.ac | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/rts/configure.ac b/rts/configure.ac
index 4a016b15a486..6a5e510db026 100644
--- a/rts/configure.ac
+++ b/rts/configure.ac
@@ -408,7 +408,7 @@ dnl See Note [Undefined symbols in the RTS]
 
 [
 symbolExtraDefs=''
-if [[ "$CABAL_FLAG_find_ptr" = 1 ]]; then
+if [ "$CABAL_FLAG_find_ptr" = 1 ]; then
     symbolExtraDefs+=' -DFIND_PTR'
 fi
 
@@ -418,7 +418,7 @@ cat $srcdir/external-symbols.list.in \
     > external-symbols.list \
     || exit 1
 
-if [[ "$CABAL_FLAG_leading_underscore" = 1 ]]; then
+if [ "$CABAL_FLAG_leading_underscore" = 1 ]; then
     sedExpr='s/^(.*)$/  "-Wl,-u,_\1"/'
 else
     sedExpr='s/^(.*)$/  "-Wl,-u,\1"/'
-- 
GitLab