Skip to content
Snippets Groups Projects
Commit 7233b3b1 authored by PHO's avatar PHO Committed by Marge Bot
Browse files

Use '[' instead of '[[' because the latter is a Bash-ism

It doesn't work on platforms where /bin/sh is something other than Bash.
parent 52c0fc69
No related branches found
No related tags found
No related merge requests found
......@@ -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"/'
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment